text:
A Tutorial on [Co-]Inductive Types in Coq
- Harold Jordan
- 2 years ago
- Views:
1 A Tutorial on [Co-]Inductive Types in Coq Eduardo Giménez, Pierre Castéran May 1998 August 17, 2007 Abstract This document 1 is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It explains how types like natural numbers and infinite streams are defined in Coq, and the kind of proof techniques that can be used to reason about them (case analysis, induction, inversion of predicates, co-induction, etc). Each technique is illustrated through an executable and self-contained Coq script. 1 The first versions of this document were entirely written by Eduardo Gimenez. Pierre Castéran wrote the 2004 revision. 1
2 Contents 1 About this document 4 2 Introducing Inductive Types Lists Vectors The contradictory proposition The tautological proposition Relations as inductive types The propositional equality type Logical connectives The existential quantifier Mutually Dependent Definitions Case Analysis and Pattern-matching Non-dependent Case Analysis Example: the predecessor function Dependent Case Analysis Example: strong specification of the predecessor function Some Examples of Case Analysis The Empty Type The Equality Type The Predicate n m Vectors Case Analysis and Logical Paradoxes The Positivity Condition Impredicative Inductive Types Extraction Constraints Strong Case Analysis on Proofs Summary of Constraints Some Proof Techniques Based on Case Analysis Discrimination of introduction rules Injectiveness of introduction rules Inversion Techniques Interactive mode Static mode Inductive Types and Structural Induction Proofs by Structural Induction Using Elimination Combinators Well-founded Recursion A case study in dependent elimination 49
3 7 Co-inductive Types and Non-ending Constructions Extensional Properties About injection, discriminate, and inversion
4 1 About this document This document is an introduction to the definition and use of inductive and co-inductive types in the Coq proof environment. It was born from the notes written for the course about the version V5.10 of Coq, given by Eduardo Gimenez at the Ecole Normale Supérieure de Lyon in March This article is a revised and improved version of these notes for the version V8.0 of the system. We assume that the reader has some familiarity with the proofs-as-programs paradigm of Logic [7] and the generalities of the Coq system [4]. You would take a greater advantage of this document if you first read the general tutorial about Coq and Coq s FAQ, both available on [5]. A text book [3], accompanied with a lot of examples and exercises [2], presents a detailed description of the Coq system and its underlying formalism: the Calculus of Inductive Construction. Finally, the complete description of Coq is given in the reference manual [4]. Most of the tactics and commands we describe have several options, which we do not present exhaustively. If some script herein uses a non described feature, please refer to the Reference Manual. If you are familiar with other proof environments based on type theory and the LCF style like PVS, LEGO, Isabelle, etc then you will find not difficulty to guess the unexplained details. The better way to read this document is to start up the Coq system, type by yourself the examples and exercises, and observe the behavior of the system. All the examples proposed in this tutorial can be downloaded from the same site as the present document. The tutorial is organised as follows. The next section describes how inductive types are defined in Coq, and introduces some useful ones, like natural numbers, the empty type, the propositional equality type, and the logical connectives. Section 3 explains definitions by pattern-matching and their connection with the principle of case analysis. This principle is the most basic elimination rule associated with inductive or co-inductive types and follows a general scheme that we illustrate for some of the types introduced in Section 2. Section 4 illustrates the pragmatics of this principle, showing different proof techniques based on it. Section 5 introduces definitions by structural recursion and proofs by induction. Section 6 presents some elaborate techniques about dependent case analysis. Finally, Section 7 is a brief introduction to co-inductive types i.e., types containing infinite objects and the principle of co-induction. Thanks to Bruno Barras, Yves Bertot, Hugo Herbelin, Jean-François Monin and Michel Lévy for their help. Lexical conventions The typewriter font is used to represent text input by the user, while the italic font is used to represent the text output by the system as answers. 4
5 Moreover, the mathematical symbols,,,,,,, and stand for the character strings <=, <>, exists, forall, ->, <-, \/, /\, and =>, respectively. For instance, the Coq statement forall A:Set,(exists x : A, forall (y:a), x <> y) -> 2 = 3 is written as follows in this tutorial: A:Set,( x:a, y:a, x y) 2 = 3 When a fragment of Coq input text appears in the middle of regular text, we often place this fragment between double quotes.... These double quotes do not belong to the Coq syntax. Finally, any string enclosed between (* and *) is a comment and is ignored by the Coq system. 2 Introducing Inductive Types Inductive types are types closed with respect to their introduction rules. These rules explain the most basic or canonical ways of constructing an element of the type. In this sense, they characterize the recursive type. Different rules must be considered as introducing different objects. In order to fix ideas, let us introduce in Coq the most well-known example of a recursive type: the type of natural numbers. Inductive nat : Set := O : nat S : nat nat. The definition of a recursive type has two main parts. First, we establish what kind of recursive type we will characterize (a set, in this case). Second, we present the introduction rules that define the type (O and S), also called its constructors. The constructors O and S determine all the elements of this type. In other words, if n:nat, then n must have been introduced either by the rule O or by an application of the rule S to a previously constructed natural number. In this sense, we can say that nat is closed. On the contrary, the type Set is an open type, since we do not know a priori all the possible ways of introducing an object of type Set. After entering this command, the constants nat, O and S are available in the current context. We can see their types using the Check command : Check nat. nat : Set Check O. O : nat Check S. S : nat nat 5
6 Moreover, Coq adds to the context three constants named nat_ind, nat_rec and nat_rect, which correspond to different principles of structural induction on natural numbers that Coq infers automatically from the definition. We will come back to them in Section 5. In fact, the type of natural numbers as well as several useful theorems about them are already defined in the basic library of Coq, so there is no need to introduce them. Therefore, let us throw away our (re)definition of nat, using the command Reset. Reset nat. Print nat. Inductive nat : Set := O : nat S : nat nat For S: Argument scope is [nat_scope] Notice that Coq s interpretation scope for natural numbers (called nat_scope) allows us to read and write natural numbers in decimal form (see [4]). For instance, the constructor O can be read or written as the digit 0, and the term S (S (S O)) as 3. Check O. 0 : nat. Check (S (S (S O))). 3 : nat Let us now take a look to some other recursive types contained in the standard library of Coq. 2.1 Lists Lists are defined in library List: Require Import List. Print list. Inductive list (A : Set) : Set := nil : list A cons : A list A list A For nil: Argument A is implicit For cons: Argument A is implicit For list: Argument scope is [type_scope] For nil: Argument scope is [type_scope] For cons: Argument scopes are [type_scope ] In this definition, A is a general parameter, global to both constructors. This kind of definition allows us to build a whole family of inductive types, indexed over the sort Set. This can be observed if we consider the type of identifiers list, cons and nil. Notice the notation (A :=...) which 6
7 must be used when Coq s type inference algorithm cannot infer the implicit parameter A. Check list. list : Set Set Check (nil (A:=nat)). nil : list nat Check (nil (A:= nat nat)). nil : list (nat nat) Check (fun A: Set (cons (A:=A))). fun A : Set cons (A:=A) : A : Set, A list A list A Check (cons 3 (cons 2 nil)). 3 :: 2 :: nil : list nat 2.2 Vectors. Like list, vector is a polymorphic type: if A is a set, and n a natural number, vector A n is the type of vectors of elements of A and size n. Require Import Bvector. Print vector. Inductive vector (A : Set) : nat Set := Vnil : vector A 0 Vcons : A n : nat, vector A n vector A (S n) For vector: Argument scopes are [type_scope nat_scope] For Vnil: Argument scope is [type_scope] For Vcons: Argument scopes are [type_scope _ nat_scope _] Remark the difference between the two parameters A and n: The first one is a general parameter, global to all the introduction rules,while the second one is an index, which is instantiated differently in the introduction rules. Such types parameterized by regular values are called dependent types. Check (Vnil nat). Vnil nat 7
8 : vector nat 0 Check (fun (A:Set)(a:A) Vcons _ a _ (Vnil _)). fun (A : Set) (a : A) Vcons A a 0 (Vnil A) : A : Set, A vector A 1 Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))). Vcons nat 5 1 (Vcons nat 3 0 (Vnil nat)) : vector nat The contradictory proposition. Another example of an inductive type is the contradictory proposition. This type inhabits the universe of propositions, and has no element at all. Print False. Inductive False : Prop := Notice that no constructor is given in this definition. 2.4 The tautological proposition. Similarly, the tautological proposition True is defined as an inductive type with only one element I: Print True. Inductive True : Prop := I : True 2.5 Relations as inductive types. Some relations can also be introduced in a smart way as an inductive family of propositions. Let us take as example the order n m on natural numbers, called le in Coq. This relation is introduced through the following definition, quoted from the standard library 2 : Print le. Inductive le (n:nat) : nat Prop := le_n: n n le_s: m, n m n S m. Notice that in this definition n is a general parameter, while the second argument of le is an index (see section 2.2). This definition introduces the 2 In the interpretation scope for Peano arithmetic: nat_scope, n <= m is equivalent to le n m. 8
9 binary relation n m as the family of unary predicates to be greater or equal than a given n, parameterized by n. The introduction rules of this type can be seen as a sort of Prolog rules for proving that a given integer n is less or equal than another one. In fact, an object of type n m is nothing but a proof built up using the constructors le_n and le_s of this type. As an example, let us construct a proof that zero is less or equal than three using Coq s interactive proof mode. Such an object can be obtained applying three times the second introduction rule of le, to a proof that zero is less or equal than itself, which is provided by the first constructor of le: Theorem zero_leq_three: subgoal 0 3 constructor 2. 1 subgoal 0 2 constructor 2. 1 subgoal 0 1 constructor 2 1 subgoal 0 0 constructor 1. Proof completed When the current goal is an inductive type, the tactic constructor i applies the i-th constructor in the definition of the type. We can take a look at the proof constructed using the command Print: Print Print zero_leq_three. zero_leq_three = 9
10 zero_leq_three = le_s 0 2 (le_s 0 1 (le_s 0 0 (le_n 0))) : 0 3 When the parameter i is not supplied, the tactic constructor tries to apply constructor 1, constructor 2,..., constructor n where n is the number of constructors of the inductive type (2 in our example) of the conclusion of the goal. Our little proof can thus be obtained iterating the tactic constructor until it fails: Lemma zero_leq_three : 0 3. repeat constructor. Notice that the strict order on nat, called lt is not inductively defined: Print lt. lt = fun n m : nat S n m : nat nat Prop Lemma zero_lt_three : 0 < 3. unfold lt. ==================== 1 3 repeat constructor. 2.6 The propositional equality type. In Coq, the propositional equality between two inhabitants a and b of the same type A, noted a = b, is introduced as a family of recursive predicates to be equal to a, parameterised by both a and its type A. This family of types has only one introduction rule, which corresponds to reflexivity. Notice that the syntax a = b is an abbreviation for eq a b, and that the parameter A is implicit, as it can be infered from a. Print eq. Inductive eq (A : Type) (x : A) : A Prop := refl_equal : x = x For eq: Argument A is implicit For refl_equal: Argument A is implicit For eq: Argument scopes are [type_scope ] For refl_equal: Argument scopes are [type_scope _] 10
11 Notice also that the first parameter A of eq has type Type. The type system of Coq allows us to consider equality between various kinds of terms: elements of a set, proofs, propositions, types, and so on. Look at [4, 3] to get more details on Coq s type system, as well as implicit arguments and argument scopes. Lemma eq_3_3 : = 3. reflexivity. Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4). reflexivity. Print eq_proof_proof. eq_proof_proof = refl_equal (refl_equal (3 * 4)) : refl_equal (2 * 6) = refl_equal (3 * 4) Lemma eq_lt_le : ( 2 < 4) = (3 4). reflexivity. Lemma eq_nat_nat : nat = nat. reflexivity. Lemma eq_set_set : Set = Set. reflexivity. 2.7 Logical connectives. The conjunction and disjunction of two propositions are also examples of recursive types: Inductive or (A B : Prop) : Prop := or_introl : A A B or_intror : B A B Inductive and (A B : Prop) : Prop := 11
12 conj : A B A B The propositions A and B are general parameters of these connectives. Choosing different universes for A and B and for the inductive type itself gives rise to different type constructors. For example, the type sumbool is a disjunction but with computational contents. Inductive sumbool (A B : Prop) : Set := left : A {A} + {B} right : B {A} + {B} This type noted {A}+{B} in Coq can be used in Coq programs as a sort of boolean type, to check whether it is A or B that is true. The values left p and right q replace the boolean values true and false, respectively. The advantage of this type over bool is that it makes available the proofs p of A or q of B, which could be necessary to construct a verification proof about the program. For instance, let us consider the certified program le_lt_dec of the Standard Library. Require Import Compare_dec. Check le_lt_dec. le_lt_dec : n m : nat, {n m} + {m < n} We use le_lt_dec to build a function for computing the max of two natural numbers: Definition max (n p :nat) := match le_lt_dec n p with left _ p right _ n end. In the following proof, the case analysis on the term le_lt_dec n p gives us an access to proofs of n p in the first case, p < n in the other. Theorem le_max : n p, n p max n p = p. intros n p ; unfold max ; case (le_lt_dec n p); simpl. 2 subgoals n : nat p : nat n p n p p = p 12
13 subgoal 2 is: p < n n p n = p trivial. intros; absurd (p < p); eauto with arith. Once the program verified, the proofs are erased by the extraction procedure: Extraction max. (** val max : nat nat nat **) let max n p = match le_lt_dec n p with Left p Right n Another example of use of sumbool is given in Section The existential quantifier. The existential quantifier is yet another example of a logical connective introduced as an inductive type. Inductive ex (A : Type) (P : A Prop) : Prop := ex_intro : x : A, P x ex P Notice that Coq uses the abreviation x:a, B for ex (fun x:a B). The former quantifier inhabits the universe of propositions. As for the conjunction and disjunction connectives, there is also another version of existential quantification inhabiting the universe Set, which is noted sig P. The syntax {x:a B} is an abreviation for sig (fun x:a B). 2.9 Mutually Dependent Definitions Mutually dependent definitions of recursive types are also allowed in Coq. A typical example of these kind of declaration is the introduction of the trees of unbounded (but finite) width: Inductive tree(a:set) : Set := node : A forest A tree A with forest (A: Set) : Set := nochild : forest A addchild : tree A forest A forest A. 13
14 Yet another example of mutually dependent types are the predicates even and odd on natural numbers: Inductive even : nat Prop := eveno : even O evens : n, odd n even (S n) with odd : nat Prop := odds : n, even n odd (S n). Lemma odd_49 : odd (7 * 7). simpl; repeat constructor. 3 Case Analysis and Pattern-matching 3.1 Non-dependent Case Analysis An elimination rule for the type A is some way to use an object a : A in order to define an object in some type B. A natural elimination for an inductive type is case analysis. For instance, any value of type nat is built using either O or S. Thus, a systematic way of building a value of type B from any value of type nat is to associate to O a constant t O : B and to every term of the form S p a term t S : B. The following construction has type B: match n return B with O t O S p t S end In most of the cases, Coq is able to infer the type B of the object defined, so the return B part can be omitted. The computing rules associated with this construct are the expected ones (the notation t S {q/p} stands for the substitution of p by q in t S :) match O return b with O t O S p t S end = t O match S q return b with O t O S p t S end = t S {q/p} Example: the predecessor function. An example of a definition by case analysis is the function which computes the predecessor of any given natural number: Definition pred (n:nat) := match n with O O S m m end. 14
15 Eval simpl in pred 56. = 55 : nat Eval simpl in pred 0. = 0 : nat Eval simpl in fun p pred (S p). = fun p : nat p : nat nat As in functional programming, tuples and wild-cards can be used in patterns. Such definitions are automatically compiled by Coq into an expression which may contain several nested case expressions. For example, the exclusive or on booleans can be defined as follows: Definition xorb (b1 b2:bool) := match b1, b2 with false, true true true, false true _, _ false end. This kind of definition is compiled in Coq as follows 3 : Print xorb. xorb = fun b1 b2 : bool if b1 then if b2 then false else true else if b2 then true else false : bool bool bool 3.2 Dependent Case Analysis For a pattern matching construct of the form match n with...end a more general typing rule is obtained considering that the type of the whole expression may also depend on n. For instance, let us consider some function Q : nat Set, and n : nat. In order to build a term of type Q n, we can associate to the constructor O some term t O : Q O and to the pattern S p some term t S : Q (S p). Notice that the terms t O and t S do not have the same type. 3 Coq uses the conditional if b then a else b as an abreviation to match b with true a false b end. 15
16 The syntax of the dependent case analysis and its associated typing rule make precise how the resulting type depends on the argument of the pattern matching, and which constraint holds on the branches of the pattern matching: Q : nat Set t O : Q O p : nat t p : Q (S p) n : nat match n as n 0 return Q n 0 with O t O S p t S end : Q n The interest of this rule of dependent pattern-matching is that it can also be read as the following logical principle (replacing Set by Prop in the type of Q): in order to prove that a property Q holds for all n, it is sufficient to prove that Q holds for O and that for all p : nat, Q holds for (S p). The former, non-dependent version of case analysis can be obtained from this latter rule just taking Q as a constant function on n. Notice that destructuring n into O or S p doesn t make appear in the goal the equalities n = O and n = S p. They are internalized in the rules above (see section 4.3.) Example: strong specification of the predecessor function. In Section 3.1.1, the predecessor function was defined directly as a function from nat to nat. It remains to prove that this function has some desired properties. Another way to proceed is to, first introduce a specification of what is the predecessor of a natural number, under the form of a Coq type, then build an inhabitant of this type: in other words, a realization of this specification. This way, the correctness of this realization is ensured by Coq s type system. A reasonable specification for pred is to say that for all n there exists another m such that either m = n = 0, or (S m) is equal to n. The function pred should be just the way to compute such an m. Definition pred_spec (n:nat) := {m:nat n=0 m=0 n = S m}. Definition predecessor : n:nat, pred_spec n. intro n; case n. n : nat pred_spec 0 unfold pred_spec;exists 0;auto. ============= n0 : nat, pred_spec (S n0) 16
17 unfold pred_spec; intro n0; exists n0; auto. Defined. If we print the term built by Coq, we can observe its dependent patternmatching structure: predecessor = fun n : nat match n as n0 return (pred_spec n0) with O exist (fun m : nat 0 = 0 m = 0 0 = S m) 0 (or_introl (0 = 1) (conj (refl_equal 0) (refl_equal 0))) S n0 exist (fun m : nat S n0 = 0 m = 0 S n0 = S m) n0 (or_intror (S n0 = 0 n0 = 0) (refl_equal (S n0))) end : n : nat, pred_spec n Notice that there are many variants to the pattern intros...; case.... Look at the reference manual and/or the book: tactics destruct, intro pattern, etc. The command Extraction can be used to see the computational contents associated to the certified function predecessor: Extraction predecessor. (** val predecessor : nat pred_spec **) let predecessor = function O O S n0 n0 Exercise 3.1 Prove the following theorem: Theorem nat_expand : n:nat, n = match n with 0 0 S p S p end. 3.3 Some Examples of Case Analysis The reader will find in the Reference manual all details about typing case analysis (chapter 4: Calculus of Inductive Constructions, and chapter 15: Extended Pattern-Matching). The following commented examples will show the different situations to consider. 17
18 3.3.1 The Empty Type In a definition by case analysis, there is one branch for each introduction rule of the type. Hence, in a definition by case analysis on p : False there are no cases to be considered. In other words, the rule of (non-dependent) case analysis for the type False is (for s in Prop, Set or Type): Q : s p : False match p return Q with end : Q As a corollary, if we could construct an object in False, then it could be possible to define an object in any type. The tactic contradiction corresponds to the application of the elimination rule above. It searches in the context for an absurd hypothesis (this is, a hypothesis whose type is False) and then proves the goal by a case analysis of it. Theorem fromfalse : False 0=1. intro H. contradiction. In Coq the negation is defined as follows : Definition not (P:Prop) := P False The proposition not A is also written A. If A and B are propositions, a is a proof of A and H is a proof of A, the term match H a return B with end is a proof term of B. Thus, if your goal is B and you have some hypothesis H : A, the tactic case H generates a new subgoal with statement A, as shown by the following example 4. Fact Nosense : = 3. intro H; case H. =========================== 0 = 0 reflexivity. The tactic absurd A (where A is any proposition), is based on the same principle, but generates two subgoals: A and A, for solving B. 4 Notice that a b is just an abreviation for a= b 18
19 3.3.2 The Equality Type Let A : Type, a, b of type A, and π a proof of a = b. Non dependent case analysis of π allows us to associate to any proof of Q a a proof of Q b, where Q : A s (where s {Prop, Set, Type}). The following term is a proof of Q a Q b. fun H : Q a match π in (_ = y) return Q y with refl_equal H end Notice the header of the match construct. It expresses how the resulting type Q y depends on the type of p. Notice also that in the pattern introduced by the keyword in, the parameter a in the type a = y must be implicit, and replaced by a wildcard _. Therefore, case analysis on a proof of the equality a = b amounts to replacing all the occurrences of the term b with the term a in the goal to be proven. Let us illustrate this through an example: the transitivity property of this equality. Theorem trans : n m p:nat, n=m m=p n=p. intros n m p eqnm. n : nat m : nat p : nat eqnm : n = m m = p n = p case eqnm. n : nat m : nat p : nat eqnm : n = m n = p n = p trivial. Exercise 3.2 Prove the symmetry property of equality. Instead of using case, we can use the tactic rewrite. If H is a proof of a = b, then rewrite H performs a case analysis on a proof of b = a, obtained by applying a symmetry theorem to H. This application of symmetry 19
20 allows us to rewrite the equality from left to right, which looks more natural. An optional parameter (either or ) can be used to precise in which sense the equality must be rewritten. By default, rewrite H corresponds to rewrite H Lemma Rw : x y: nat, y = y * x y * x * x = y. intros x y e; do 2 rewrite <- e. 1 subgoal x : nat y : nat e : y = y * x y = y reflexivity. Notice that, if H : a = b, then the tactic rewrite H replaces all the occurrences of a by b. However, in certain situations we could be interested in rewriting some of the occurrences, but not all of them. This can be done using the tactic pattern. Let us consider yet another example to illustrate this. Let us start with some simple theorems of arithmetic; two of them are already proven in the Standard Library, the last is left as an exercise. mult_1_l : n : nat, 1 * n = n mult_plus_distr_r : n m p : nat, (n + m) * p = n * p + m * p mult_distr_s : n p : nat, n * p + p = (S n)* p. Let us now prove a simple result: Lemma four_n : n:nat, n+n+n+n = 4*n. intro n;rewrite <- (mult_1_l n). n : nat 1 * n + 1 * n + 1 * n + 1 * n = 4 * (1 * n) 20
21 We can see that the rewrite tactic call replaced all the occurrences of n by the term 1 * n. If we want to do the rewriting ony on the leftmost occurrence of n, we can mark this occurrence using the pattern tactic: Undo. intro n; pattern n at 1. n : nat (fun n0 : nat n0 + n + n + n = 4 * n) n Applying the tactic pattern n at 1 allowed us to explicitly abstract the first occurrence of n from the goal, putting this goal under the form Q n, thus pointing to rewrite the particular predicate on n that we search to prove. rewrite <- mult_1_l. 1 subgoal n : nat 1 * n + n + n + n = 4 * n repeat rewrite mult_distr_s. n : nat 4 * n = 4 * n trivial The Predicate n m The last but one instance of the elimination schema that we will illustrate is case analysis for the predicate n m: Let n and p be terms of type nat, and Q a predicate of type nat Prop. If H is a proof of n p, H 0 a proof of Q n and H S a proof of m:nat, n m Q (S m), then the term match H in (_ q) return (Q q) with le_n H0 le_s m Hm HS m Hm end 21
22 is a proof term of Q p. The two patterns of this match construct describe all possible forms of proofs of n m (notice again that the general parameter n is implicit in the in... clause and is absent from the match patterns. Notice that the choice of introducing some of the arguments of the predicate as being general parameters in its definition has consequences on the rule of case analysis that is derived. In particular, the type Q of the object defined by the case expression only depends on the indexes of the predicate, and not on the general parameters. In the definition of the predicate, the first argument of this relation is a general parameter of the definition. Hence, the predicate Q to be proven only depends on the second argument of the relation. In other words, the integer n is also a general parameter of the rule of case analysis. An example of an application of this rule is the following theorem, showing that any integer greater or equal than 1 is the successor of another natural number: Lemma predecessor_of_positive : n, 1 n p:nat, n = S p. intros n H;case H. n : nat H : 1 n p : nat, 1 = S p exists 0; trivial. n : nat H : 1 n m : nat, 0 m p : nat, S m = S p intros m _. exists m. trivial Vectors The vector polymorphic and dependent family of types will give an idea of the most general scheme of pattern-matching. For instance, let us define a function for computing the tail of any vector. 22
23 Notice that we shall build a total function, by considering that the tail of an empty vector is this vector itself. In that sense, it will be slightly different from the Vtail function of the Standard Library, which is defined only for vectors of type vector A (S n). The header of the function we want to build is the following: Definition Vtail_total (A : Set) (n : nat) (v : vector A n) : vector A (pred n):= Since the branches will not have the same type (depending on the parameter n), the body of this function is a dependent pattern matching on v. So we will have : match v in (vector _ n0) return (vector A (pred n0)) with The first branch deals with the constructor Vnil and must return a value in vector A (pred 0), convertible to vector A 0. So, we propose: Vnil Vnil A The second branch considers a vector in vector A (S n0) of the form Vcons A n0 v0, with v0:vector A n0, and must return a value in vector A (pred (S n0)), convertible to v0:vector A n0. This second branch is thus : Vcons _ n0 v0 v0 Here is the full definition: Definition Vtail_total (A : Set) (n : nat) (v : vector A n) : vector A (pred n):= match v in (vector _ n0) return (vector A (pred n0)) with Vnil Vnil A Vcons _ n0 v0 v0 end. 3.4 Case Analysis and Logical Paradoxes In the previous section we have illustrated the general scheme for generating the rule of case analysis associated to some recursive type from the definition of the type. However, if the logical soundness is to be preserved, certain restrictions to this schema are necessary. This section provides a brief explanation of these restrictions. 23
CHAPTER 7 GENERAL PROOF SYSTEMS 1 Introduction Proof systems are built to prove statements. They can be thought as an inference machine with special statements, called provable statements, or sometimesMore information
Mathematical Induction
Mathematical Induction In logic, we often want to prove that every member of an infinite set has some feature. E.g., we would like to show: N 1 : is a number 1 : has the feature Φ ( x)(n 1 x! 1 x) HowMore information
Chapter II. Controlling Cars on a Bridge
Chapter II. Controlling Cars on a Bridge 1 Introduction The intent of this chapter is to introduce a complete example of a small system development. During this development, you will be made aware of theMore information
OPERATIONAL TYPE THEORY by Adam Petcher Prepared under the direction of Professor Aaron Stump A thesis presented to the School of Engineering of
WASHINGTON NIVERSITY SCHOOL OF ENGINEERING AND APPLIED SCIENCE DEPARTMENT OF COMPTER SCIENCE AND ENGINEERING DECIDING JOINABILITY MODLO GROND EQATIONS IN OPERATIONAL TYPE THEORY by Adam Petcher PreparedMore information
[Refer Slide Time: 05:10]
Principles of Programming Languages Prof: S. Arun Kumar Department of Computer Science and Engineering Indian Institute of Technology Delhi Lecture no 7 Lecture Title: Syntactic Classes Welcome to lectureMore information
ML for the Working Programmer
ML for the Working Programmer 2nd edition Lawrence C. Paulson University of Cambridge CAMBRIDGE UNIVERSITY PRESS CONTENTS Preface to the Second Edition Preface xiii xv 1 Standard ML 1 Functional ProgrammingMore information
Termination Checking: Comparing Structural Recursion and Sized Types by Examples
Termination Checking: Comparing Structural Recursion and Sized Types by Examples David Thibodeau Decemer 3, 2011 Abstract Termination is an important property for programs and is necessary for formal proofsMore information
CS510 Software Engineering
CS510 Software Engineering Propositional Logic Asst. Prof. Mathias Payer Department of Computer Science Purdue University TA: Scott A. Carr Slides inspired by Xiangyu Zhang http://nebelwelt.net/teaching/15-cs510-seMore information
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic
Parametric Domain-theoretic models of Linear Abadi & Plotkin Logic Lars Birkedal Rasmus Ejlers Møgelberg Rasmus Lerchedahl Petersen IT University Technical Report Series TR-00-7 ISSN 600 600 February 00More information
3. Mathematical Induction
3. MATHEMATICAL INDUCTION 83 3. Mathematical Induction 3.1. First Principle of Mathematical Induction. Let P (n) be a predicate with domain of discourse (over) the natural numbers N = {0, 1,,...}. If (1)More information
263-2200 Types and Programming Languages
263-2200 Types and Programming Languages 1 / 49 Outline Types Evaluation Rules Typing Rules Properties of the Typing Relation The Inversion Lemma Prolog Implementation Reasoning Involving Types ProgressMore information
A first step towards modeling semistructured data in hybrid multimodal logic
A first step towards modeling semistructured data in hybrid multimodal logic Nicole Bidoit * Serenella Cerrito ** Virginie Thion * * LRI UMR CNRS 8623, Université Paris 11, Centre d Orsay. ** LaMI UMRMore information
Deterministic Discrete Modeling
Deterministic Discrete Modeling Formal Semantics of Firewalls in Isabelle/HOL Cornelius Diekmann, M.Sc. Dr. Heiko Niedermayer Prof. Dr.-Ing. Georg Carle Lehrstuhl für Netzarchitekturen und NetzdiensteMore information
CHAPTER 3. Methods of Proofs. 1. Logical Arguments and Formal Proofs
CHAPTER 3 Methods of Proofs 1. Logical Arguments and Formal Proofs 1.1. Basic Terminology. An axiom is a statement that is given to be true. A rule of inference is a logical rule that is used to deduceMore information
POLYTYPIC PROGRAMMING OR: Programming Language Theory is Helpful
POLYTYPIC PROGRAMMING OR: Programming Language Theory is Helpful RALF HINZE Institute of Information and Computing Sciences Utrecht University Email: email@example.com Homepage: http://www.cs.uu.nl/~ralf/More information
2. Methods of Proof Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try.
2. METHODS OF PROOF 69 2. Methods of Proof 2.1. Types of Proofs. Suppose we wish to prove an implication p q. Here are some strategies we have available to try. Trivial Proof: If we know q is true thenMore information
Verifying Specifications with Proof Scores in CafeOBJ
Verifying Specifications with Proof Scores in CafeOBJ FUTATSUGI, Kokichi 二 木 厚 吉 Chair of Language Design Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)More information
Likewise, we have contradictions: formulas that can only be false, e.g. (p p).
CHAPTER 4. STATEMENT LOGIC 59 The rightmost column of this truth table contains instances of T and instances of F. Notice that there are no degrees of contingency. If both values are possible, the formulaMore information
Adding GADTs to OCaml the direct approach
Adding GADTs to OCaml the direct approach Jacques Garrigue & Jacques Le Normand Nagoya University / LexiFi (Paris) https://sites.google.com/site/ocamlgadt/ Garrigue & Le Normand Adding GADTs to OCaml 1More information
So let us begin our quest to find the holy grail of real analysis.
1 Section 5.2 The Complete Ordered Field: Purpose of Section We present an axiomatic description of the real numbers as a complete ordered field. The axioms which describe the arithmetic of the real numbersMore information
PROCEEDINGS OF THE YEREVAN STATE UNIVERSITY Physical and Mathematical Sciences 2012 1 p. 43 48 ON FUNCTIONAL SYMBOL-FREE LOGIC PROGRAMS I nf or m at i cs L. A. HAYKAZYAN * Chair of Programming and InformationMore information
the type checking problem (TCP) schema the proof checking problem the type synthesis problem (TSP) decidability input: Γ M :? polymorphism in Coq
schema the type checking problem (TCP) decidability polymorphism in Coq dependent inductive data-types in Coq further reading overview input: Γ M : N? output: true yes the typing judgement is derivableMore information
A Propositional Dynamic Logic for CCS Programs
A Propositional Dynamic Logic for CCS Programs Mario R. F. Benevides and L. Menasché Schechter {mario,firstname.lastname@example.com Abstract This work presents a Propositional Dynamic Logic in which the programs areMore information
Formal Languages and Automata Theory - Regular Expressions and Finite Automata -
Formal Languages and Automata Theory - Regular Expressions and Finite Automata - Samarjit Chakraborty Computer Engineering and Networks Laboratory Swiss Federal Institute of Technology (ETH) Zürich MarchMore information
PROGRAM-ing Finger Trees in COQ
PROGRAM-ing Finger Trees in COQ Matthieu Sozeau Univ. Paris Sud, CNRS, Laboratoire LRI, UMR 8623, Orsay, F-91405 INRIA Futurs, ProVal, Parc Orsay Université, F-91893 email@example.com Abstract Finger TreesMore information
Handout #1: Mathematical Reasoning
Math 101 Rumbos Spring 2010 1 Handout #1: Mathematical Reasoning 1 Propositional Logic A proposition is a mathematical statement that it is either true or false; that is, a statement whose certainty orMore information
This asserts two sets are equal iff they have the same elements, that is, a set is determined by its elements.
3. Axioms of Set theory Before presenting the axioms of set theory, we first make a few basic comments about the relevant first order logic. We will give a somewhat more detailed discussion later, butMore information
Elementary Number Theory We begin with a bit of elementary number theory, which is concerned
CONSTRUCTION OF THE FINITE FIELDS Z p S. R. DOTY Elementary Number Theory We begin with a bit of elementary number theory, which is concerned solely with questions about the set of integers Z = {0, ±1,More information
Journal of Functional Programming, volume 3 number 4, 1993. Dynamics in ML
Journal of Functional Programming, volume 3 number 4, 1993. Dynamics in ML Xavier Leroy École Normale Supérieure Michel Mauny INRIA Rocquencourt Abstract Objects with dynamic types allow the integrationMore information
M.Sc. program in mathematics INTRODUCTORY SET THEORY Katalin Károlyi Department of Applied Analysis, Eötvös Loránd University H-1088 Budapest, Múzeum krt. 6-8. CONTENTS 1. SETS Set, equal sets, subset,More information
Chapter 7: Functional Programming Languages
Chapter 7: Functional Programming Languages Aarne Ranta Slides for the book Implementing Programming Languages. An Introduction to Compilers and Interpreters, College Publications, 2012. Fun: a languageMore information
The Foundations: Logic and Proofs. Chapter 1, Part III: Proofs
The Foundations: Logic and Proofs Chapter 1, Part III: Proofs Rules of Inference Section 1.6 Section Summary Valid Arguments Inference Rules for Propositional Logic Using Rules of Inference to Build ArgumentsMore information
Automated Theorem Proving - summary of lecture 1
Automated Theorem Proving - summary of lecture 1 1 Introduction Automated Theorem Proving (ATP) deals with the development of computer programs that show that some statement is a logical consequence ofMore information
Mathematics for Computer Science/Software Engineering. Notes for the course MSM1F3 Dr. R. A. Wilson
Mathematics for Computer Science/Software Engineering Notes for the course MSM1F3 Dr. R. A. Wilson October 1996 Chapter 1 Logic Lecture no. 1. We introduce the concept of a proposition, which is a statementMore information
WHAT ARE MATHEMATICAL PROOFS AND WHY THEY ARE IMPORTANT? introduction Many students seem to have trouble with the notion of a mathematical proof. People that come to a course like Math 216, who certainlyMore information
Formal Engineering for Industrial Software Development
Shaoying Liu Formal Engineering for Industrial Software Development Using the SOFL Method With 90 Figures and 30 Tables Springer Contents Introduction 1 1.1 Software Life Cycle... 2 1.2 The Problem 4 1.3More information
Discrete Mathematics and Probability Theory Fall 2009 Satish Rao, David Tse Note 2
CS 70 Discrete Mathematics and Probability Theory Fall 2009 Satish Rao, David Tse Note 2 Proofs Intuitively, the concept of proof should already be familiar We all like to assert things, and few of usMore information
Rigorous Software Development CSCI-GA 3033-009
Rigorous Software Development CSCI-GA 3033-009 Instructor: Thomas Wies Spring 2013 Lecture 11 Semantics of Programming Languages Denotational Semantics Meaning of a program is defined as the mathematicalMore information
Correspondence analysis for strong three-valued logic
Correspondence analysis for strong three-valued logic A. Tamminga abstract. I apply Kooi and Tamminga s (2012) idea of correspondence analysis for many-valued logics to strong three-valued logic (K 3 ).More information
Dependent Types at Work
Dependent Types at Work Ana Bove and Peter Dybjer Chalmers University of Technology, Göteborg, Sweden {bove,email@example.com Abstract. In these lecture notes we give an introduction to functional programmingMore information
Continued Fractions and the Euclidean Algorithm
Continued Fractions and the Euclidean Algorithm Lecture notes prepared for MATH 326, Spring 997 Department of Mathematics and Statistics University at Albany William F Hammond Table of Contents IntroductionMore information
Summary Last Lecture. Automated Reasoning. Outline of the Lecture. Definition sequent calculus. Theorem (Normalisation and Strong Normalisation)
Summary Summary Last Lecture sequent calculus Automated Reasoning Georg Moser Institute of Computer Science @ UIBK Winter 013 (Normalisation and Strong Normalisation) let Π be a proof in minimal logicMore information
Equality and dependent type theory. Oberwolfach, March 2 (with some later corrections)
Oberwolfach, March 2 (with some later corrections) The Axiom of Univalence, a type-theoretic view point In type theory, we reduce proof-checking to type-checking Hence we want type-checking to be decidableMore information
Monitoring Metric First-order Temporal Properties
Monitoring Metric First-order Temporal Properties DAVID BASIN, FELIX KLAEDTKE, SAMUEL MÜLLER, and EUGEN ZĂLINESCU, ETH Zurich Runtime monitoring is a general approach to verifying system properties atMore information
Theory of Computation Lecture Notes
Theory of Computation Lecture Notes Abhijat Vichare August 2005 Contents 1 Introduction 2 What is Computation? 3 The λ Calculus 3.1 Conversions: 3.2 The calculus in use 3.3 Few Important Theorems 3.4 WorkedMore information
Math 3000 Section 003 Intro to Abstract Math Homework 2
Math 3000 Section 003 Intro to Abstract Math Homework 2 Department of Mathematical and Statistical Sciences University of Colorado Denver, Spring 2012 Solutions (February 13, 2012) Please note that theseMore information
Fundamental Computer Science Concepts Sequence TCSU CSCI SEQ A
Fundamental Computer Science Concepts Sequence TCSU CSCI SEQ A A. Description Introduction to the discipline of computer science; covers the material traditionally found in courses that introduce problemMore information
Static Typing for Object-Oriented Programming
Science of Computer Programming 23(1):19 53, 1994. Static Typing for Object-Oriented Programming Jens Palsberg email@example.com Michael I. Schwartzbach email@example.com Computer Science DepartmentMore information
Moving from CS 61A Scheme to CS 61B Java
Moving from CS 61A Scheme to CS 61B Java Introduction Java is an object-oriented language. This document describes some of the differences between object-oriented programming in Scheme (which we hope youMore information
Foundational Proof Certificates
An application of proof theory to computer science INRIA-Saclay & LIX, École Polytechnique CUSO Winter School, Proof and Computation 30 January 2013 Can we standardize, communicate, and trust formal proofs?More information
This chapter is all about cardinality of sets. At first this looks like a
CHAPTER Cardinality of Sets This chapter is all about cardinality of sets At first this looks like a very simple concept To find the cardinality of a set, just count its elements If A = { a, b, c, d },More information
Software Engineering
Software Engineering Lecture 04: The B Specification Method Peter Thiemann University of Freiburg, Germany SS 2013 Peter Thiemann (Univ. Freiburg) Software Engineering SWT 1 / 50 The B specification methodMore information
Regression Verification: Status Report
Regression Verification: Status Report Presentation by Dennis Felsing within the Projektgruppe Formale Methoden der Softwareentwicklung 2013-12-11 1/22 Introduction How to prevent regressions in softwareMore information
The following themes form the major topics of this chapter: The terms and concepts related to trees (Section 5.2).
CHAPTER 5 The Tree Data Model There are many situations in which information has a hierarchical or nested structure like that found in family trees or organization charts. The abstraction that models hierarchicalMore information
Elementary Number Theory and Methods of Proof. CSE 215, Foundations of Computer Science Stony Brook University http://www.cs.stonybrook.
Elementary Number Theory and Methods of Proof CSE 215, Foundations of Computer Science Stony Brook University http://www.cs.stonybrook.edu/~cse215 1 Number theory Properties: 2 Properties of integers (wholeMore information
Reading 13 : Finite State Automata and Regular Expressions
CS/Math 24: Introduction to Discrete Mathematics Fall 25 Reading 3 : Finite State Automata and Regular Expressions Instructors: Beck Hasti, Gautam Prakriya In this reading we study a mathematical modelMore information
Turing Degrees and Definability of the Jump. Theodore A. Slaman. University of California, Berkeley. CJuly, 2005
Turing Degrees and Definability of the Jump Theodore A. Slaman University of California, Berkeley CJuly, 2005 Outline Lecture 1 Forcing in arithmetic Coding and decoding theorems Automorphisms of countableMore information
Degrees of Truth: the formal logic of classical and quantum probabilities as well as fuzzy sets.
Degrees of Truth: the formal logic of classical and quantum probabilities as well as fuzzy sets. Logic is the study of reasoning. A language of propositions is fundamental to this study as well as trueMore information
We would like to state the following system of natural deduction rules preserving falsity:
A Natural Deduction System Preserving Falsity 1 Wagner de Campos Sanz Dept. of Philosophy/UFG/Brazil email@example.com Abstract This paper presents a natural deduction system preserving falsity. This newMore information
Mathematical Induction
Mathematical Induction (Handout March 8, 01) The Principle of Mathematical Induction provides a means to prove infinitely many statements all at once The principle is logical rather than strictly mathematical,More information
SQL INJECTION ATTACKS By Zelinski Radu, Technical University of Moldova
SQL INJECTION ATTACKS By Zelinski Radu, Technical University of Moldova Where someone is building a Web application, often he need to use databases to store information, or to manage user accounts. AndMore information
Computing and Informatics, Vol. 20, 2001,????, V 2006-Nov-6 UPDATES OF LOGIC PROGRAMS Ján Šefránek Department of Applied Informatics, Faculty of Mathematics, Physics and Informatics, Comenius University,More information
each college c i C has a capacity q i - the maximum number of students it will admit
n colleges in a set C, m applicants in a set A, where m is much larger than n. each college c i C has a capacity q i - the maximum number of students it will admit each college c i has a strict order iMore information
THE TURING DEGREES AND THEIR LACK OF LINEAR ORDER JASPER DEANTONIO Abstract. This paper is a study of the Turing Degrees, which are levels of incomputability naturally arising from sets of natural numbers.More information
Regular Languages and Finite Automata
Regular Languages and Finite Automata 1 Introduction Hing Leung Department of Computer Science New Mexico State University Sep 16, 2010 In 1943, McCulloch and Pitts [4] published a pioneering work on aMore information
E3: PROBABILITY AND STATISTICS lecture notes
E3: PROBABILITY AND STATISTICS lecture notes 2 Contents 1 PROBABILITY THEORY 7 1.1 Experiments and random events............................ 7 1.2 Certain event. Impossible event............................More information
Symbol Tables. Introduction
Symbol Tables Introduction A compiler needs to collect and use information about the names appearing in the source program. This information is entered into a data structure called a symbol table. TheMore information
2. The Language of First-order Logic
2. The Language of First-order Logic KR & R Brachman & Levesque 2005 17 Declarative language Before building system before there can be learning, reasoning, planning, explanation... need to be able toMore information
InvGen: An Efficient Invariant Generator
InvGen: An Efficient Invariant Generator Ashutosh Gupta and Andrey Rybalchenko Max Planck Institute for Software Systems (MPI-SWS) Abstract. In this paper we present InvGen, an automatic linear arithmeticMore information
CHAPTER 3 Numbers and Numeral Systems
CHAPTER 3 Numbers and Numeral Systems Numbers play an important role in almost all areas of mathematics, not least in calculus. Virtually all calculus books contain a thorough description of the natural,More information
Introduction to Automata Theory. Reading: Chapter 1
Introduction to Automata Theory Reading: Chapter 1 1 What is Automata Theory? Study of abstract computing devices, or machines Automaton = an abstract computing device Note: A device need not even be aMore information
A single minimal complement for the c.e. degrees
A single minimal complement for the c.e. degrees Andrew Lewis Leeds University, April 2002 Abstract We show that there exists a single minimal (Turing) degree b < 0 s.t. for all c.e. degrees 0 < a < 0,More information
Predicate Logic. For example, consider the following argument:
Predicate Logic The analysis of compound statements covers key aspects of human reasoning but does not capture many important, and common, instances of reasoning that are also logically valid. For example,More information
Relations: their uses in programming and computational specifications
PEPS Relations, 15 December 2008 1/27 Relations: their uses in programming and computational specifications Dale Miller INRIA - Saclay & LIX, Ecole Polytechnique 1. Logic and computation Outline 2. ComparingMore information
Computing Concepts with Java Essentials
2008 AGI-Information Management Consultants May be used for personal purporses only or by libraries associated to dandelon.com network. Computing Concepts with Java Essentials 3rd Edition Cay HorstmannMore information
(LMCS, p. 317) V.1. First Order Logic. This is the most powerful, most expressive logic that we will examine.
(LMCS, p. 317) V.1 First Order Logic This is the most powerful, most expressive logic that we will examine. Our version of first-order logic will use the following symbols: variables connectives (,,,,More information
Factoring & Primality
Factoring & Primality Lecturer: Dimitris Papadopoulos In this lecture we will discuss the problem of integer factorization and primality testing, two problems that have been the focus of a great amountMore information
Chapter 2: Problem Solving Using C++
Chapter 2: Problem Solving Using C++ 1 Objectives In this chapter, you will learn about: Modular programs Programming style Data types Arithmetic operations Variables and declaration statements CommonMore information
Finite Sets. Theorem 5.1. Two non-empty finite sets have the same cardinality if and only if they are equivalent.
MATH 337 Cardinality Dr. Neal, WKU We now shall prove that the rational numbers are a countable set while R is uncountable. This result shows that there are two different magnitudes of infinity. But weMore information
Predicate Calculus. There are certain arguments that seem to be perfectly logical, yet they cannot be expressed by using propositional calculus.
Predicate Calculus (Alternative names: predicate logic, first order logic, elementary logic, restricted predicate calculus, restricted functional calculus, relational calculus, theory of quantification,More information
Mathematical Induction. Lecture 10-11
Mathematical Induction Lecture 10-11 Menu Mathematical Induction Strong Induction Recursive Definitions Structural Induction Climbing an Infinite Ladder Suppose we have an infinite ladder: 1. We can reachMore information
Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation
Under consideration for publication in J. Functional Programming 1 Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation EDWIN BRADY School of Computer Science, UniversityMore information
THE SEARCH FOR NATURAL DEFINABILITY IN THE TURING DEGREES ANDREW E.M. LEWIS 1. Introduction This will be a course on the Turing degrees. We shall assume very little background knowledge: familiarity withMore information
Regular Expressions with Nested Levels of Back Referencing Form a Hierarchy
Regular Expressions with Nested Levels of Back Referencing Form a Hierarchy Kim S. Larsen Odense University Abstract For many years, regular expressions with back referencing have been used in a varietyMore information
Which Semantics for Neighbourhood Semantics?
Which Semantics for Neighbourhood Semantics? Carlos Areces INRIA Nancy, Grand Est, France Diego Figueira INRIA, LSV, ENS Cachan, France Abstract In this article we discuss two alternative proposals forMore information
Verifying security protocols using theorem provers
1562 2007 79-86 79 Verifying security protocols using theorem provers Miki Tanaka National Institute of Information and Communications Technology Koganei, Tokyo 184-8795, Japan Email: firstname.lastname@example.com information
Consistency, completeness of undecidable preposition of Principia Mathematica. Tanmay Jaipurkar
Consistency, completeness of undecidable preposition of Principia Mathematica Tanmay Jaipurkar October 21, 2013 Abstract The fallowing paper discusses the inconsistency and undecidable preposition of PrincipiaMore information
The Goldberg Rao Algorithm for the Maximum Flow Problem
The Goldberg Rao Algorithm for the Maximum Flow Problem COS 528 class notes October 18, 2006 Scribe: Dávid Papp Main idea: use of the blocking flow paradigm to achieve essentially O(min{m 2/3, n 1/2 }More information
Cartesian Products and Relations
Cartesian Products and Relations Definition (Cartesian product) If A and B are sets, the Cartesian product of A and B is the set A B = {(a, b) :(a A) and (b B)}. The following points are worth specialMore information
On automating the extraction of programs from termination proofs
On automating the extraction of programs from termination proofs Fairouz Kamareddine, François Monin Mauricio Ayala-Rincón Abstract We investigate an automated program synthesis system that is based onMore information
CHAPTER 2. Logic. 1. Logic Definitions. Notation: Variables are used to represent propositions. The most common variables used are p, q, and r.
CHAPTER 2 Logic 1. Logic Definitions 1.1. Propositions. Definition 1.1.1. A proposition is a declarative sentence that is either true (denoted either T or 1) or false (denoted either F or 0). Notation:More information
Removing Partial Inconsistency in Valuation- Based Systems*
Removing Partial Inconsistency in Valuation- Based Systems* Luis M. de Campos and Serafín Moral Departamento de Ciencias de la Computación e I.A., Universidad de Granada, 18071 Granada, Spain This paperMore information
arxiv:0804.4490v1 [math.gm] 28 Apr 2008
Infinite sequences in the framework of classical logic arxiv:0804.4490v1 [math.gm] 28 Apr 2008 V.V. Ivanov N.N. Semenov Institute of Chemical Physics, Russian Academy of Sciences, Kosygin str.4, Moscow,More information
Predicate Logic Review
Predicate Logic Review UC Berkeley, Philosophy 142, Spring 2016 John MacFarlane 1 Grammar A term is an individual constant or a variable. An individual constant is a lowercase letter from the beginningMore information
Testing LTL Formula Translation into Büchi Automata
Testing LTL Formula Translation into Büchi Automata Heikki Tauriainen and Keijo Heljanko Helsinki University of Technology, Laboratory for Theoretical Computer Science, P. O. Box 5400, FIN-02015 HUT, FinlandMore information
Formal Verification Coverage: Computing the Coverage Gap between Temporal Specifications
Formal Verification Coverage: Computing the Coverage Gap between Temporal Specifications Sayantan Das Prasenjit Basu Ansuman Banerjee Pallab Dasgupta P.P. Chakrabarti Department of Computer Science & EngineeringMore information
University of Ostrava. Reasoning in Description Logic with Semantic Tableau Binary Trees
University of Ostrava Institute for Research and Applications of Fuzzy Modeling Reasoning in Description Logic with Semantic Tableau Binary Trees Alena Lukasová Research report No. 63 2005 Submitted/toMore information
A binary search tree or BST is a binary tree that is either empty or in which the data element of each node has a key, and:
Binary Search Trees 1 The general binary tree shown in the previous chapter is not terribly useful in practice. The chief use of binary trees is for providing rapid access to data (indexing, if you will)More information
Theory of Computation Prof. Kamala Krithivasan Department of Computer Science and Engineering Indian Institute of Technology, Madras
Theory of Computation Prof. Kamala Krithivasan Department of Computer Science and Engineering Indian Institute of Technology, Madras Lecture No. # 31 Recursive Sets, Recursively Innumerable Sets, EncodingMore information
A Semantical Perspective on Verification of Knowledge
A Semantical Perspective on Verification of Knowledge Paul Leemans, Jan Treur, Mark Willems Vrije Universiteit Amsterdam, Department of Artificial Intelligence De Boelelaan 1081a, 1081 HV Amsterdam TheMore information


text:
Call us at (541) 308-1800 for a new-and-improved version of our Buisness Membership information. We know you will love the changes!
1600 Air Museum Rd. Hood River, OR 97031
(541) 308-1600
Open Daily 9 - 5 Closed: Thanksgiving Day, Christmas Day, New Years Day
Let us help you plan your visit.
WAAAM was recently donated a 1930 Stearman 6! Check out the journey it took to fly here below.Read more ...
Congratulations to Dale Nicol!Read more ...
We're ranked #7 in all of Oregon by visitors! Thanks!Read more ...
WAAAM History - Photos - Stories - Info
Many volunteer opportunities are available. Here is a partial list of how you can get involved.
Find out more on our volunteer page.
There are several levels of membership available to individuals and families.
Call (541) 308-1600 for information on Business Memberships.

subset: commoncrawl


text:
What Is "Spice"? Is It Different From Bath Salts? by Eliza Player
Synthetic drugs have been a hot topic in the news lately, with stories covering the various bans of these drugs, as well as stories of the effects of these drugs on its users. The types of synthetic drugs fall into two different categories, bath salts and synthetic marijuana. These are very different drugs, although many of the news reports simply lump them together. I think that lumping them together does a disservice to the public, as we are not properly educated about these substances.
This week, I have scoured the Internet for stories about these synthetic drugs. Although I have found some alarming stories about synthetic marijuana, many of the stories involving bath salts are more horrific. Synthetic marijuana has been reported to cause some mild psychosis, as well as rapid heartbeat, high blood pressure, and high body temperatures. Bath salts, on the other hand, often involve extreme hallucinations, often inciting violence.
I am, by no means, trying to say synthetic pot is ok and it is not harmful…but I do think that bath salts are much more dangerous. Bath salts are a type of methamphetamine; where as synthetic marijuana is closer to pot. I think that any research into these two substances will validate my opinion.
So, what is synthetic marijuana? Just like the name suggests, it is synthetically made compound that mimics the effects of marijuana. These chemicals are similar to the natural cannabinoids found in marijuana. The chemical is made in a liquid form, and then it is put onto herbs to be smoked. These drugs come prepackaged and ready to smoke. Like bath salts, the packaging states that it is "not for human consumption."
These "herbal blends" are sold in head shops around the country, under names like K2 and Spice. The drug is often referred under these names. As more bans on synthetic drugs are put into place, these drugs are slowly becoming harder to obtain. Like bath salts, though, chemists come up with new formulas for the active ingredient, slightly different than the banned chemicals. These new chemicals also produce a marijuana-like high, but are not banned under the current law. The DEA has taken steps to ban 5 compounds often found in synthetic marijuana, but chemists have created more than 5 formulas.
Some sources believe that synthetic marijuana is stronger than the real thing, and these sources also site that it is more dangerous. In recent years, calls to poison control about synthetic marijuana have been on the rise. One doctor and researcher claims that these substances can cause an increased risk of paranoia and disorganized behavior. Evidence shows that extremely large doses of "Spice" may produce some negative effects not associated with marijuana, such as increased agitation and vomiting. People are not, however, thinking their baby is a demon and dropping them off on the interstate. People are not, however, attacking police officers and stabbing them multiple times. And people are not biting police cruisers hard enough to leave marks as a result of synthetic marijuana use. All of these things have been attributed to the use of bath salts.
Image courtesy of TheRecordHerald.com.


text:
We didn't want it to have to come to this, but it's time for Sufferlandria to be recognised by the International Olympic Committee.
We're attaching the following letter to a Sufferlandrian Pigeon and sending it to Switzerland tonight.
Click on image to read full size.
Get unlimited access to 37 Sufferfest videos, 20 yoga for cyclists videos, 10 different training plans and more. Train to specific fitness targets by connecting your power meter, HR strap and trainer using real or virtual power. Control your smart trainer. One subscription works across Windows, Mac, iPad and iPhone devices. Try it for free for 7 days. Cancel easily at any time. If you continue, it's just $10 USD/month.


text:
It takes great people to make a great company, and at Woodfin, our people are the best - and it's no accident. Our belief in the importance of quality people is reflected in the way we hire, train and reward employees. We hire hard-working people who understand the importance of customer service. We then give these hard working folks the training and equipment they need to be highly effective in their jobs. We understand how important a great customer experience is to you!
About Us
Our Management team has over 300 years of combined experience in all sorts of home services and maintenance needs, such as oilheat, heating and air conditioning, electrical, plumbing, security and more. We feel nothing prepares you like experience. Knowing how vast our vast experience is both in the field and behind the scenes, you can rest assured that when you choose Woodfin you choose the best, most experienced team in Richmond. We've heard it all and seen it all!
Our Technicians
Woodfin technicians perform installation, service and repairs with confidence and competence because they have the knowledge and the tools that the job requires. At Woodfin, we share our institutional knowledge and work together to solve every problem without delay. At our in-house training center, we constantly train our Woodfin technicians in teaching new skills and learning how to service and properly maintain new equipment. We employ technicians certified by NATE (The North American Technician Excellence), meaning our Woodfin techs are well prepared with real working knowledge of HVAC and HVACR systems.
Our Customer Service Team
Woodfin has the best customer service team in Richmond..and we stand firmly behind that statement! Outstanding customer service is the corner stone of why we've grown and succeeded where other have not. We strive to provide you with nothing but the most friendly, knowledgeable, empathetic and helpful service. These days...a lot of people prefer to handle their business online as opposed to calling us directly, so to stay abreast with current customer demands we've created a Live Online Help system (check to see if we're online in the upper right of your screen). Our customer service representatives undergo monthly training to ensure you receive the utmost in customer service.
Our Leadership Team
All of us at Woodfin dedicate ourselves daily to your home comfort. Our LEADERSHIP TEAM accepts nothing less:
JACK WOODFIN, CEO & President - Woodfin Heating Inc
JUSTIN R. ANDRESS, President - Woodfin Oil
KEVIN W. WALSH, Chief Financial Officer
DAVID A. KIBILOSKI, Corporate Treasurer
A. PENN STAPLES - General Manager - Petroleum Products
TRAVIS D. RIDDLE - General Manager - Mechanical Services
ROBBIE LEE - Sales Manager - Mechanical Services
H. O. HARCUM - Director of Retail Operations - Pit Stop Stores
CHIP HARDY - Operations Manager - Security & Home Automation
DONALD L. GIRARD - Service Manager - HVAC
DANNY SHACKELFORD - Service Manager - Plumbing
WAYNE H. GROFF, JR - HVAC Installations Manager
ROBERT R. SNYDER - Service Manager - Electrical
ALAN BARRETT - Delivery Operations Manager
We look forward to the opportunity to faithfully serve your A/C, Heating, oil heat, electric, plumbing and security needs for years to come!
Call us at 804-730-5000 to discuss your specific needs or to setup a new account, or contact us online and we will get back to you ASAP!
Our Community


text:
The Leading eBooks Store Online
3,935,953 members ⚫ 1,292,914 ebooks
New to eBooks.com?Learn more
- Bestsellers - This Week
- Foreign Language Study
- Pets
- Bestsellers - Last 6 months
- Games
- Philosophy
- Archaeology
- Gardening
- Photography
- Architecture
- Graphic Books
- Poetry
- Art
- Health & Fitness
- Political Science
- Biography & Autobiography
- History
- Psychology & Psychiatry
- Body Mind & Spirit
- House & Home
- Reference
- Business & Economics
- Humor
- Religion
- Children's & Young Adult Fiction
- Juvenile Nonfiction
- Romance
- Computers
- Language Arts & Disciplines
- Science
- Crafts & Hobbies
- Law
- Science Fiction
- Current Events
- Literary Collections
- Self-Help
- Drama
- Literary Criticism
- Sex
- Education
- Literary Fiction
- Social Science
- The Environment
- Mathematics
- Sports & Recreation
- Family & Relationships
- Media
- Study Aids
- Fantasy
- Medical
- Technology
- Fiction
- Music
- Transportation
- Folklore & Mythology
- Nature
- Travel
- Food and Wine
- Performing Arts
- True Crime
- Foreign Language Books
Most popular at the top
Pot FarmUNP - Nebraska Paperback 2012; US$ 16.95
After eight months in his childhood home helping his mother through her bout with cancer, Matthew Frank and his wife were themselves desperate for comfort. They found sanctuary in the most unlikely place—amid a collection of outcasts and eccentrics on a plot of land miles outside their comfort zone: a "mostly medical" marijuana farm in California.... more...
Global Uncertainty and the Volatility of Agricultural Commodities PricesIOS Press 2012; US$ 196.00
The recent global financial crisis exposed the serious limitations of existing economic and financial models. Not only did macro models fail to predict the crisis, they seemed incapable of explaining what was happening to the economy. Policymakers felt abandoned by the conventional tools of the now obsolete Washington consensus and the World Trade... more...
The Rice Industry of Burma 1852-1940 (First Reprint 2012)Institute of Southeast Asian Studies 2012; US$ 64.90
This study forms a welcome addition to the growing number of works on the economic history of Southeast Asia. In his Foreword, Dr John F. Cady, the author of A History of Modern Burma, writes that Dr Cheng "has placed all students of Burma in her debt by this highly articulate and clarifying contribution to the country's economic history". more...
Seed Trade in Rural MarketsTaylor and Francis 2009; US$ 53.95
Markets have been found to be an increasingly important source of the seeds of crops and varieties low income farmers need to improve their livelihoods, encompassing both the formal and informal seed sector. Markets also have major impacts on agricultural biodiversity, by affecting farmers' choice of crops and varieties to grow. They are not, however,... more...
WeinkonsumSpringer Fachmedien Wiesbaden 2012; US$ 35.63
Wein ist in unserer Gesellschaft sowohl in kultureller als auch ökonomischer Hinsicht von beträchtlicher Bedeutung. Vor dem Hintergrund möglicher gesellschaftlicher Entstrukturierungsprozesse und unter Berücksichtigung der Eigenschaften des Weines als ästhetisierbarem Konsumgut untersucht Simone Pape, welcher Wein getrunken wird, auf welche Art und... more...
Fundraising gegen HungerkrisenSpringer Fachmedien Wiesbaden 2012; US$ 9.63
Hängen Preisanstiege bei Nahrungsmitteln wirklich monokausal mit der monetären Spekulation auf die sog. "Commodities" zusammen? Wo haben große NPO wie UNICEF ihre Stärken, wo ihre Schwächen? Wie kann Fundraising effektiv betrieben werden? Was sollte unternommen werden, um Armut und Hunger in der Welt tatsächlich zu reduzieren? Auf diese und weitere... more...
Animal farming and environmental interactions in the Mediterranean regionWageningen Academic Publishers 2012; US$ 84.82
This book focuses on animal-environment interactions in the Mediterranean region, and the impact of human activities on the type and magnitude of these interactions. Evaluates the economic, social and environmental aspects of sustainable livestock production. more...
Alcohol And Emerging MarketsTaylor and Francis 2013; US$ 54.95
Divided into two parts, Alcohol and Emerging Markets begins with a series of case studies that assess alcohol issues in four regions - Asia, Central and Eastern Europe, Latin America, and Sub-Saharan Africa - and four countries - China, India, Mexico, and Russia. Issues such as past and current public policy developments, prevention programs, and... more...
LocalHarperCollins 2014; US$ 23.99
Combining stunning visuals with insights and a lexicon of more than 200 agricultural terms explained by today's thought leaders, Local showcases and explores one of the most popular environmental trends: rebuilding local food movements. When Douglas Gayeton took his young daughter to see the salmon run—a favorite pastime growing up in Northern California—he... more...
The Brewers Association's Guide to Starting Your Own BreweryBrewers Publications 2013; US$ 94.99
The Brewers Association's Guide to Starting Your Own Brewery delivers essential industry insight needed by aspiring brewers. This comprehensive guide covers everything from site selection and branding to regulatory requirements and equipment considerations. Industry veteran Dick Cantwell of Elysian Brewing covers ingredients, financing, business... more...


text:
Oak Foundation commits its resources to address issues of global social and environmental concern, particularly those that have a major impact on the lives of the disadvantaged.
National Center for Missing and Exploited Children
The National Center for Missing and Exploited Children (NCMEC) a non—profit 501(c)(3) corporation whose mission is to help find missing children, reduce child sexual exploitation, and prevent child victimization.
UNICEF is a leading humanitarian and development agency working globally for the rights of every child.
INHOPE coordinates a network of Internet Hotlines all over the world, supporting them in responding to reports of illegal content to make the Internet safer.
ICMEC - the International Centre for Missing and Exploited Children - advocates, trains and collaborates to eradicate child abduction, sexual abuse and exploitation.
The Interactive Generations Forum (Foro Generaciones Interactivas) was born in December 2008 with this idea in mind, founded by Telefónica, the University of Navarra and the Inter-American Organization for Higher Education Organization.
We're responding by applying our technology, ingenuity, and collaborative spirit to help solve these critical challenges and create fulfilling and exciting opportunities for people everywhere.
Resurgens Foundation is a Swiss-based foundation. The Foundation will contribute, in particular, to the development of programmes and support to organizations promoting free and honest use of information technologies, seeking to combat the damaging aspects of these information technologies and helping those who have been victims of swindles and other fraudulent behavior on the Internet.
ECPAT International is a global network of organisations working together for the elimination of child prostitution, child pornography and the trafficking of children for sexual purposes. It seeks to ensure that children everywhere enjoy their fundamental rights free and secure from all forms of commercial sexual exploitation.


text:
While the Congress was busy discussing military intervention in Syria in its first public hearing on Tuesday, Senator John McCain was caught on camera playing poker on his phone.
Here's a photo:
Yes, that is @SenJohnMcCain playing poker on his iPhone. Hero! http://t.co/PXhXpkQyqD pic.twitter.com/IntcVADHzB— David Beard (@dabeard) September 3, 2013
McCain (R-Arizona) is one of the many U.S. politicians who want President Barack Obama to strike Syria in order to put an end to Bashar al Assad's atrocities on his people. In an interview to Fox News on Sunday, McCain said, "The only way you're gonna solve this is help those people overthrow Bashar al-Assad."
Related: Here Is What Obama And Other U.S. Politicians Are Saying About Intervention In Syria (VIDEOS)
McCain also said referring to the chemical bombing in Syria, "You saw these pictures of these dead children. Come on. This is horrific. We can't stand by and watch this happen."
But the poker episode suggests otherwise.
John McCain posted the following tweet after learning that he had been caught (with proof) that he wasn't really interested in the Congress meeting:
Scandal! Caught playing iPhone game at 3+ hour Senate hearing - worst of all I lost!— John McCain (@SenJohnMcCain) September 3, 2013
A very interesting reply was tweeted to him:
Read: John McCain Accidentally Takes Photo With Syrian Kidnapper


text:
Blinder begins the conclusion of his book with Ten Financial Commandments. The first is Thou Shalt Remember That People Forget. This is the reason Geithner gave for rushing to introduce new financial rules after he took office as Barack Obama's Treasury secretary in January, 2009. Market gurus such as George Soros complained that officials were moving too fast, but the political window to do so is only as wide as voters' memories.
Geithner and others were right to worry. The bank lobby in Washington not only fought to delay the enactment of Dodd-Frank in January, 2010, but continues to fight through the process of writing and implementing specific rules. A surprising number of Republican lawmakers would happily scrap it even now. The Obama administration's ability to fight the crisis was also restrained by an already-bloated budget deficit. As surpluses under Bill Clinton turned to deficits under George W. Bush in the early 2000s, politicians forgot that one of the main reasons governments should run surpluses is so they are able to provide shelter when the rains come. Yet Democratic and Republican lawmakers still would rather score political points than balance the books.
In the post-crisis years, it's become fashionable to reflect on the teachings of Hyman Minksy, an American economist who died in 1996. Minksy believed financial markets were prone to euphoria — and forgetfulness. Stability led to risk, which led to debt. And debt brought everything crashing down. This is the root of Dimon's fatalism. There is something in the human condition that pulls us to the brink. There will be more crises and new lessons. But that's not an excuse for allowing history to repeat itself. Bernanke, Carney and others have helped to improve the New Testament theory of business cycles. The challenge now is to commit its lessons to memory.
March 17, 2008
Shares of the 158-year-old investment bank Lehman Bros. fall by 48% after news that Bear Stearns has been bought by JPMorgan for $2 a share. Dick Fuld, who has been Lehman's CEO since 1993, makes an appearance on the bank's trading floor to boost morale — "the only time he did that in the last six months of the firm," according to one Canadian trader. "It was like seeing Elvis or Madonna, because otherwise, you never saw the guy." The shares bounce back the next day
Sept. 10
Lehman investment bank posts a $3.9-billion loss in the third quarter, after writing down $5.6 billion in toxic mortgages. Fuld and CFO Erin Callan also announce that the brokerage firm has raised $6-billion in fresh capital. Its share price falls by 10%
Sept. 11
Barclays announces it is considering buying Lehman, joining another potential bidder, Bank of America. Lehman's shares fall by 13.5%
Sept. 12
Moody's warns it could downgrade Lehman's credit rating if the bank doesn't find a "stronger financial partner"
Sept. 14
Over the weekend, 100 Wall Street bankers, regulators and Treasury officials meet at the New York Fed to discuss Lehman's future. Treasury refuses to cough up more bailout money. Barclays withdraws its bid for Lehman; Bank of America follows suit within hours. Alan Greenspan warns that if Lehman goes, "we will see other major firms fail."
Sept. 14
Ten of the biggest investment banks put together a liquidity pool of $70 billion that any of them can tap
Sept. 15, 1 a.m.
Lehman files for Chapter 11 bankruptcy. With $639 billion in assets and $619 billion in debt, it is the largest corporate bankruptcy in U.S. history. Lehman's 25,000 employees worldwide start packing their boxes
Sept. 15, 8 a.m.
Bank of America announces it will rescue Merrill Lynch in a $50-billion buyout
Sept. 15
The S&P 500 falls 4.7%, its worst showing since the market reopened after the Sept. 11, 2001, attacks. Financial stocks have their worst day ever, down more than 10%
Sept. 16
Barclays swoops in to buy Lehman's U.S. business for $2-billion
Sept. 17
The Fed announces an $85-billion rescue of AIG, giving taxpayers an 80% stake in the insurer
May 14, 2009
Fuld, whose compensation totalled roughly $500-million between 2000 and 2008, finally leaves the bank with no severance or bonus
Report Typo/Error
Follow @CarmichaelKevinon Twitter:
- Goldman Sachs Group Inc$220.18-2.12(-0.95%)
- American International Group Inc$64.20-0.03(-0.05%)
- JMP Group Inc$5.35+0.05(+0.94%)
- Updated July 21 4:00 PM EDT. Delayed by at least 15 minutes.


text:
Surviving Congo's civil war, being resurrected. It is hard to believe how people treat each other. It is even harder to understand how humans can be so destructive towards fellow humans. Then it is even harder to realize that in Africa, the tribal customs and racial divides there became civil wars and the atrocities are unbelieveable.
From Idi Amin in Uganda many years ago to the Hutus and Tutsis fighting each other; it is a study in how low people can go. The hate and then the racial barriers for many people today can only be described as devilish. I have covered many such things and it is never easy to figure out the hate. The hearts of those who do such things are blackened, no love, no mercy, implacable.
WIBR/WARN Commentary on Surviving Congo's civil war, being resurrected
Now read this, Surviving Congo's civil war, being resurrected
Daniel Kanyarahuru hid in the roof of his home when forces loyal to Congo's President Laurent Kabila stormed his village in Kasai-Oriental province hunting for ethnic Tutsis. The teenager's brother, his wife, and their one-month-old baby were taken away by soldiers. "It was the middle of the night. There was a lot of brutality. I saw…
Surviving Congo's civil war, being resurrected
Alert: Attention the Battle we Face
Be sure to check out the latest "The Battle We Face" a endtime focus for Remnant Believers in Jesus Christ!
Disclaimer: The WIBR/WARN Radio and Ministry provides Articles and news from many sources; This is a service to our readers and listeners. We do not necessarily agree with the viewpoints given in the articles and while we provide said content provided by republish and/or others, we cannot verify that all facts are true or verified.
***The articles that we publish represent the viewpoints of the authors and not the WIBR/WARN radio websites and ministry. We offer commentary and points on the articles themselves and we sign them as such. But the articles following are those of the authors themselves and not the WIBR/WARN.
WIBR/WARN Radio is an end time, preaching, teaching, advocacy, and warning agency heralding in the second coming of Jesus Christ to this earth. We cover many news items on the persecuted church and are advocates for those being persecuted overseas. We also promote and let you know of those agencies that work directly with the persecuted church so you can directly give to them.
While WIBR/WARN provides for donations to our ministry, we do not collect donations for other agencies, nor do we receive money from those agencies we promote. We are also not connected to them but by faith and purpose in order to aid those in the field.
The WIBR/WARN Radio utilizes syndication to move content throughout the system for more people to be able to obtain. We also provide content of our own, articles by the Watchman Dana G Smith, and Biblical in-depth teachings by the Watchman Dana G Smith. These are easily found through syndication of our material.
On our websites, material is free, but these are connected to a syndication process which is separate from our professionally published materials. These published materials like our books, e-books, and such may not be free and are covered with copyright and are sold as such through Amazon or other booksellers.
WIBR/WARN Websites are www.warn-usa.com, www.warn-radio.com, www.wingswatchman.org and have been combined into one large resource depository. These websites endorse the Watchman Dana G Smith and are the biblical viewpoints according to the Word of God.
Dana G Smith maintains a professional Writers site and hub. You can find Dana's writer's website at www.danaglennsmith.com which will feature books, reviews, articles, commentaries written and syndicated by him.
Surviving Congo's civil war, being resurrected
Special Warn Radio Study Series
The complete series in one place, Some not all our Teachings! We have years and years worth!
First, though;Don't miss our extensive, modern, and very versatile Archives!
Find The Warn-USA Archives here
Find The WingsWatchman.org Archives here
Anti-Christ Shadows of Nations
Blood and Blood guilt Murderer's Row
Dunamis of Acts series Exegesis
"Held in Contempt of the Lords Court"
Prophecy Defining the End of Days
The High, Exalted One and His People
Colossians "Centricity of Christ"
Revelation Series Exegesis page where we have the complete volume of teachings pertaining to the "Time is at Hand"
Deuteronomy Series Exogesis In 14 parts for the Remnant
Patriarch Remnant Series selection of teachings on Israel, Moses, Abraham, Isaac, Judah, Roots Remnant
Surviving Congo's civil war, being resurrected
WIBR/WARN Radio Specialty Blogs Plus
The Variety, Articles, Shows, and News
World News Blog
Surviving Congo's civil war, being resurrected
About WIBR/WARN Radio page here
WIBR/WARN Radio is an endtime, preaching, teaching, advocacy, and warning agency heralding in the second coming of Jesus Christ to this earth. We publish this information for the Believers in Christ Jesus to pray, be informed, support, and help those brethren in Christ overseas who are persecuted. We also recommend you support those agencies who directly work and or support these persecuted believers.
Surviving Congo's civil war, being resurrected
The WIBR/WARN Radio network and the Remnant
Many years ago we started out in college broadcasting over our college transmitter. Then we broadcast into 150 nations over World Harvest Shortwave Radio and World Wide Christian Radio
Today, we are still moving forward with the gospel. We are the Watchman Institute of Biblical Research and the Watchman Alert Radio network.
WIBR/WARN Current Broadcasts
Surviving Congo's civil war, being resurrected
Tuesdays 7-9 pm mst Remnant Battle Lines
Surviving Congo's civil war, being resurrected
Fridays 7-9 pm mst Sound the Shofar
Surviving Congo's civil war, being resurrected
Warn Radio Listen Live pages and other info
Warn Radio Blogtalkradio page
Our WIBR/WARN Chat page, Listen
The Watchman Video site
Surviving Congo's civil war, being resurrected


text:
What Cake Works Well Under Fondant???
Decorating By mpowelljones Updated 15 Oct 2010 , 6:49pm by brincess_b
I'm sure this has already been asked somewhere, but I wasn't sure how to query for the answer. At any rate, I'm wondering what type of cake works the best under fondant? I'm thinking probably a butter cake because it's more dense, but I wonder what you all think?
Pretty much anything will do. I use victoria, maderia and pound cake, carrot cake, fruit cake.... As long as it's not really soft like angel food.
Pretty much anything will do. I use victoria, maderia and pound cake, carrot cake, fruit cake.... As long as it's not really soft like angel food.
agree, pretty much anything but angel food. Angel food is just to light and airy to hold up to the weight of fondant (even if it's rolled really really thin)
I've used straight from the box mix cakes and they held up fine.
Thanks for the help everybody.
What about the frosting? Is there a particular frosting that works better? What about IMBC? Is that a good one?
Any frosting is good, it depends what u like eating and working with.
Imbc or smbc are generally less sweet, and non crusting.
Traditional bc can be made with butter or crisco (and ps and liquid) - crisco holds up better to the heat, and it will crust. Then u have other recipes like indydebis (that I use) or sugarshacks, which must be the most popular recipes on here.
Some people use ganache too, sets up very firm for getting sharp corners.
Quote by @%username% on %date%


text:
Perfect Lashes everytime
All good products and ideas usually stem from a desire to deliver a solution to a problem. TK's Lashes have stamped their authority well and truly in the cosmetics market and TK's Lashes Dance are Queensland's answer to Long Lashes for the Dance Industry. For too long dancers have had to endure glue and lashes that fall off on stage. Not only is it time consuming and messy but dangerous given glue residue could make it's way to the eye.
A simple process
TK's Lashes Dance have kept the application simple. Apply the transplant gel first to your clean lashes and follow this up with the TK's Lashes fibre brush to elongate your lashes. Reapply the transplanting gel to set your lashes. You can re-apply further and the impact you get will be bigger. In fact, up to 3 times your original lash length. Totally amazing!
The product is safe to use and the impact is outstanding. For a dancer, it's one of those products that shares equal footing with your tights, shoes and leotard. TK's Lashes are a must for all dancers.
TK's Lashes Dance also offer the product to schools to use as a fundraising item. Great volume discounts apply.
For further information view their website.


text:
St. Johnsville, New York
United States New York Montgomery CountyTown of St. Johnsville
Church Records
- Records of the Dutch Reformed Saint John's Church: In the Town of St. Johnsville, Montgomery County, N.Y. 2 vols. New York, 1914. Digital version at Ancestry ($).
- Records of the Dutch Reformed Saint John's Church: In the Town of St. Johnsville, Montgomery County, N.Y. 2 vols. New York, 1914. Digital version at Ancestry ($).
Archives, Libraries and Museums
Library and Museum
Margaret Reaney Memorial Library and Museum
19 Kingsbury Avenue
St. Johnsville, New York 13452
Phone: 518-568-7822
The Palatine Settlement Society
P.O. Box 183
St. Johnsville, New York 13452
Email: firstname.lastname@example.com
Town Clerk
St. Johnsville Town Clerk
7431 State Highway 5
P.O. Box 28
Saint Johnsville, New York 13452
Phone: 518-568-2662
Email: email@example.com
Town Historian
St. Johnsville Town Historian
7 Center Street
St. Johnsville, New York 13452,
;Phone: 518-568-2910
Email: email@example.com
Town Records
To locate additional published and transcribed records for St. Johnsville, New York check:
- Gordon L. Remington, New York Towns, Villages, and Cities: A Guide to Genealogical Sources (Boston: New England Historic Genealogical Society, 2002). American Ancestors online edition; At various libraries (WorldCat); FHL Book 974.7 D27r. Alphabetical list including date founded, if a town history exists, church and cemetery sources, and if a Civil War register (TCR) exists. The codes used under Church and Cemetery are defined in the link above the listing of towns, cities and villages.
Vital Records


text:
NCR's 5th Annual Webathon: Day Two begins with a matching grant. Your $500 or $100 could become $100 or $200 if you act now. Make a donation.
Vatican City -- Wrapping up decades of change, conflict, Francis canonizes two popes Read NCR's complete coverage of the papal canonizations
Canonization of predecessors provides another boost for Pope Francis
Manila, Philippines -- Filipinos fill stadium coliseum to celebrate Mass for new saints. Cardinal Antonio Tagle tells them, The one beside you can be a saint
Catholic school teachers in Cincinnati, Oakland and Hawaii see new clauses in their contracts: Contracts defining teachers as ministers raise labor questions
Seattle -- Labor board: Adjunct professors at Catholic university can form union
JACKSON, Miss. -- In conservative Mississippi, some business owners who support equal treatment for gays and lesbians are pushing back against a new law that bans government from limiting the free practice of religion. Business window stickers protest Mississippi law
The religious left is struggling. Can the cause of economic justice help it rise again?
Utrecht, Netherlands -- Second dead Dutch bishop found guilty of sex abuse of minors
Buffalo, N.Y. -- Catholic high school won't put gay grad's wedding news in alumni magazine Girls academy says its following bishop's instructions.
Monongahela, Pa. -- A group of parishioners has abandoned a sit-in to protest the closing of a Roman Catholic church outside Pittsburgh.
Green Bay, Wis. -- Church calls cellphone tower a 'beacon' to draw worshippers Opponents are worried that the communications system — designed to look like a church steeple — would harm property values and create possible health hazards in the neighborhood.
Archbishop of Canterbury: Empty churches show UK is NOT Christian
Looking for a little inspiration to begin your day? NCR's sister publication, Celebration, gives you two options, both based on the Scripture readings of the day:
Pencil Preaching is blog in which Celebration editor Pat Marrin combines Scripture and sketching to reflect on the Word.
Daily Bread is a series of short reflections written by four authors who meet regularly to share the readings. Daily Bread is intended to help daily preachers and others who pray from the assigned Scriptures each day to orient themselves to the Living Word addressed to the church in the world. It's a great way to begin the day.
NCR Comment code: (Comments can be found below)
Before you can post a comment, you must verify your email address at Disqus.com/verify.
Comments from unverified email addresses will be deleted.
- Be respectful. Do not attack the writer. Take on the idea, not the messenger.
- Don't use obscene, profane or vulgar language.
- Stay on point. Comments that stray from the original idea will be deleted. NCR reserves the right to close comment threads when discussions are no longer productive.
We are not able to monitor every comment that comes through. If you see something objectionable, please click the "Report abuse" button. Once a comment has been flagged, an NCR staff member will investigate.
For more detailed guidelines, visit our User Guidelines page.
For help on how to post a comment, visit our reference page.
Commenting is available during business hours, Central time, USA. Commenting is not available in the evenings, over weekends and on holidays. More details are available here. Comments are open on NCR's Facebook page.


text: Drinking can lead to erection problems. The desire contributes to erection dysfunction, although alcoholic drink frequently increases it by reducing hang-ups. These can additionally lessen your want for sexual activity. Being physically inactive also contributes to the odds of impotency. Why Every 2nd matters with HBP! 1. The most crucial action to take is retain your passwords a key. If a password must be given by you to someone, make sure to alter it when they can be finished utilizing the Best Site To Buy Viagra access. Don't write your passwords down or reveal them with also many individuals. Occasionally change your passwords. Make use of an on-line password generator that is powerful. 2. In child-molestation cases it is the standard procedure to have medical examinations completed within 72 hours of the alleged molestations, the severe phase of the claimed occasions, to get forensic evidence-epidermis, hair, sperm, spit, etc, from the penile areas. What Dr. Vibrant found was that no history of occasions was taken by the examiners to establish the degree of assessment needed for each victim which is really essential. For the millions of Americans who are under-insured or uninsured, the out of pocket cost to purchase prescription drugs Viagra 100mg Online may put a strain on their standard of living as well as a household's funds. Occasionally, households need to choose from purchasing drugs as well as other monetary requirements. That's why the difference may fill preventing individuals from being forced to make the tough choice regarding whether to buy other of life's requirements or drugs. Actually discount drugstores in the USA don't supply the prescription medications that is affordable that the online pharmacies that are finest offer. Do keep in mind look at this web-page that a lot of nutritional supplements out there contained Acai are extremely low-quality. That's merely a truth. Most manufacturers don't wish since they recognize that the vast majority of the buyers do not know the huge difference anyway to pay a lot of money on ingredients. But this really is really wrong. In the event the products include the finest raw materials accessible, the results will be noticed by the consumers and return for more. March 27th 1998 turned out to be an amazing evening for treating male impotence. The FDA alleviated the suffering of several millions of guys authorized the sale and accreditation of blue pill and, in the process. This recent discovery is just yet another reason for guys to consider blue pill as an answer to their problems. Don't dress like a bum - even though this may appear clear and comical to some, a straightforward glimpse around any check my source pub / nightclub by any girl trust me!, may show several completely naive men dressed like drivel. Now don't-get me wrong and the goal isn't to attempt to not seem poor or well-off as possible - built only to be well presented. Today, there is large variety of nutritional supplements available, to increase the size of length and hardon of sexual activities. Countless man sufferings from impotence or Erectile Dysfunction home ED get helpful hints confused in choosing the right nutritional supplement, in increasing their erection, which will help them effectively. And Viagra, one of typically the most popular one of them has become synonymous to greatest treatment of impotence. Your dog farms and dog business did very well out of the as they were not unable to charge costs that are Hop Over To This Webpage high for his or her meat due to its exceptionally potent capacity. Men may go to the countryside to banquet on containers of canine meat or bones, the price changing from pricey to ludicrous, and then come back to the city to visit prostitutes and enjoyment girls, persuaded in their bodily capabilities, which are now additionally enhanced by their ingesting of inexpensive, potent japanese wine. After a night of eating, drinking and visiting enjoyment houses, they are going to get back house totally covered, and be yelled at by their wives, as they also drunkenly try to mount.