Logic and Applications 
Ferenczi, M. Szots, M.
2010

0.1 Preface 
This is the preface. 
0.1. PREFACE

1. Introduction 
2. Proof theory 
2.1 Natural deduction

2.2 Normal forms

2.3 Reducing satisﬁability

2.4 Resolution calculus

2.5. Automated theorem proving

3. Logic programming 
3.1. Programming with deﬁnite clauses

3.2. On deﬁniability

3.3. General paradigm of logic programming

3.4. Problems and trends

4. Program speciﬁcation and veriﬁcation 
4.1 General introduction

4.2 Formal theories

4.3 Logic based software technologies

5. Knowledge based systems 
5.1 Nonmonotonic reasoning

5.2 Plausible inference

5.3. Great projects in reasonings

6. Logic and complexity theory 

References 
2

Chapter 1

INTRODUCTION

Spreading of computers implied suddenly a large change in the position of logic: it has become an applied science, a part of applied mathematics. Concepts, results and methods of logic got importance in computer science. Logic has become an important device in artiﬁcial intelligence, in program speciﬁcation and veriﬁcation, in formal languages, in automata theorem proving, in algorithm theory, etc. The role of logic in computer science is twofold: 
The one is that logic helps the foundation of several ﬁelds of computer science. Its main reason is that logic is the only discipline which studies meaning in a strict formal way (that is in mathematical way). This is why logic today is widely recognized to be one of the fundamental discipline of computing and problem solving (maybe the most important one). 
The other role of logic in information systems is that logic serves not only a theory, but languages and calculi of logic can be formed into direct tools of software development technologies (VDM, Z, HOL, TLA+ and so on), database systems and knowledge representation. Special logics can be used even as programming languages (like PROLOG, DATALOG). 
Present paper organically continues [22]. We intend to show how logics introduced there help solving problems in some ﬁeld of computer science we are sorry to say that complete review cannot be provided in a paper, volumes of handbooks are needed (see [27], from [1] to [6], from [28] to [32]). In present paper some interesting classes of problems to be discussed are selected as 
•	how formal semantics can be provided for programming languages? 
•	how to make certain that programs (or other dynamic systems) behaves as it is intended (how to verify them)? 
•	how to how to represent knowledge in a formal way? 

However no complete study can be given even for the selected topics the basic notions, some interesting aspects and approaches are discussed Similarly, because the lack of space, we can not detail some important areas of applications as databases theory, functional programming, logic design etc. 
3 
We use the concepts introduced in [22] and try to use the same notation. 
I say thanks to Miklos Ferenczi and Gabor Sagi for their advice and useful notices. I am indebted to Gergely Budai who helped me to navigate in the state of art of program veriﬁcation tools. 
Chapter 2

Proof theory

Proof theory plays an important role in many applications of logic, e.g. in logic programming, in program speciﬁcations, etc. In this Section we sketch two proof systems: the deduction system natural deduction and the refutation system resolution. This latter is the base of PROLOG and historically, it was the base of automatic theorem proving. 
2.1 Natural deduction 
The origin of this calculus goes back to [33], we present it in the form as it is presented in [76]. This calculus reﬂects the construction of mathematical proofs. 
First we treat the inference rules of the system. For any logical symbol there are inference rules of two types: 
•	introduction rule: this rule produces a formula from formulas in terms of 
αβ 
logical symbol, like α∧β; 
•	elimination rule: this rule dissects a formula eliminating a logical symbol, like α∧β .
α 
The following Table includes the inference rules of Natural deduction. If Cis a connective or a quantiﬁer, the corresponding elimination and introduction rules are denoted by CE and CI respectively. 
Syntax is expanded by symbol ⊥ to denote falsity, and by an enumerable set of constants {ai∈ω. In the table t, t1, t2 are terms of the expanded language. 
}i
In rule =E it is allowed to substitute only some occurrences of t1 by t2, in the other cases xi/t means that all occurrences of xi are to be substituted by 
t. In rules ∀I and ∃E the constant aj is used with the condition that it occurs neither in the assumptions of the derivation of β[xi/aj] and of the subderivation β[xi/aj] γ respectively, nor in the conclusion γ.
⇒
As examples we explain the rules ∨E and I from the Table. 
→
The meaning of the ∨E rule is: If the premiss is α ∨ β, further a proof of γ from α, and a proof of γ from β are given, then we can conclude γ. The 
5 Table 2.1: Rules of Natural Deduction 
∧I: 	α β α ∧ β 	∧E: 	α ∧ β α α ∧ β β 	
∨I: 	α α ∨ β β α ∨ β 	∨E: 	[α] [β] ⇓ ⇓α ∨ β γ γ γ 	
→I 	[a] ⇓β α → β 	→E 	α α → β β 	
	[α] 		[¬α] 	
	⇓ 		⇓ 	
¬I 	⊥ ¬α 	¬E 	⊥ α 	
⊥I 	α ¬α ⊥ 	⊥E 	⊥ α 	
∀I: 	β(xi/aj ) ∀xiβ 	∀E: 	∀xiβ β(xi/t) 	
∃I 	β(xi/t) ∃xiβ 	∃E: 	β[xi/aj ] ⇓ ∃xiβ γ γ 	
=I 	t = t 	=E 	t1 = t2 α α(t1/t2) 	

2.1. NATURAL DEDUCTION 7 
formalized version of this inference has also to include proofs of γ from α and β respectively. ,,The proof of γ from α” is denoted by [α]= γ (the notation 
⇒
will occur vertically in the rules). The two proofs of γ depend on α and β respectively, however neither α nor β is a premiss of the whole inference. So if the two ,,subproofs” gets into the proof of γ from disjunction α ∨ β, assumptions α and β have to be discharged (cancelled). Brackets [] denote discharging. 
Let us consider the of →I rule. The elimination rule for implication is Modus Ponens, but how to prove α → β ? The meaning of the →I rule is: if there is a derivation of β from α (i.e. [α] β ) then αβ can be considered to 
⇒→
be proved. By Deduction Theorem this rule is expected to be correct. Clearly while α is a premiss of the derivation of β, α is not a premiss of αβ, so α has to be discharged. → 
If a rule includes the discharge of a formula, only some occurrences have to be discharged, maybe none of them (so discharge is a possibility, but not an obligation). 
The ¬E rule, the formal version of ,,reductio ad absurdum”, is sometimes questioned in mathematics as well as in logics. If it is omitted, intuitionistic logic is obtained. This rule is equivalent to the ,,excluded middle”principle. If even the rule ⊥E is omitted, then proof system of the so called minimal logic is obtained. 
In Natural Deduction a proof of a formula α from a set of formulas Σ has a tree structure. The root of the tree is labeled by formula α, elements of Σ may label some leaves, some leaves may be labeled by a discharged formula. The other nodes can be constructed using the inference rules. We do not deﬁne exactly here the structure of Natural Deduction proofs, but two proofs are given as examples; namely the proofs of the universal validity of formulae .αα and ∃xi¬→ ¬¬
α → ¬∀xiα. 
To understand the derivations the discharged formulae and the step when they are discharged are marked by the same index. 
2
[¬α]1 [α]⊥I 
1
⊥ I 
α ¬2
¬¬I 
αα →
→ ¬¬
In the second example elimination rules are also used. Notice that ﬁrst the elimination rules are used, and after these the introduction rules. 
2
[∀xiα]
[α(xi/a)]1 α(xi/a) ∀E
¬
3
[∃xi¬α]
1
⊥⊥I ∃E 
2
⊥ I 
3
¬∀xiα ¬I
→
∃xi¬α → ¬∀xiα 
The Natural Deduction proof system is complete for the semantical consequence relation of ﬁrst order classical logic. If the ¬E rule is omitted, it is complete for intuisitionistic semantical consequence relation. 
An important problem in proof theory is the existence of so called normal form of a proof, the simplest derivation. Note that the inference rules have a kind of symmetry the elimination and introduction rules can be considered as the inverses of each other. The application of an elimination rule to a formula obtained by its inverse introduction rules is superﬂuous. In normal form such pairs are not allowed. More formally, each ,,path”1 of a normal derivation consists of a (maybe empty) sequence of applications of introduction rules and after it a (maybe empty) sequence of applications of elimination rules. 
The following proposition (the basic theorem of proof theory) holds: Every derivation can be transformed into a normal form. 

2.2 Normal forms 
As a preparation for resolution we survey the normal forms of ﬁrst order logic. Formulas can be manipulated easier using these ,,canonical” forms. 
Deﬁnition 1 (prenex normal form) 
If a formula α is of the form Q1x1 ...Qnxnα�, where Qi can be universal or existential quantiﬁer, and α� is quantiﬁer free formula, it is called to be in prenex normal form. 
The sequence of quantiﬁcations Q1x1 ...Qnxn is called the prenex ( or preﬁxum), formula α’ is called the matrix (or the kernel ) of α. 
For every ﬁrst order formula there is an equivalent one in prenex normal form. We remark that prenex normal forms of a formula are not unique. 
The next normal form is a simpliﬁcation of prenex normal form by eliminating existential quantiﬁers. 
Notice that in a given model the truth of ∀x1∃y1α means the existence of a function Y1(x) such that ∀x1α(y1/Y1(x1)) is true in this model. The underlying idea of universal Skolem normal form is that the language is expanded by function a function symbol to denote function Y1. The function symbols introduced so are called Skolem functions. 
Deﬁnition 2 (Skolem normal form) 
Let α be a sentence in prenex normal form. The following algorithm generates the Skolem normal form of α: 
1.	If the prenex of α consists of only universal quantiﬁers, the algorithm stops, α is in Skolem normal form. 
2.	Let α be of the form ∀x1 ...∀xj ∃yiβ for some j and i. Let us expand the language by an jary function symbol Yi which do not occur in the alphabet of the language, and let α be substituted by ∀x1 ...∀xj β(yi/Yi(x1,...xj )). 

1The deﬁnition of the notion of path in a Natural Deduction proof is complicated, that is why we do not give it here. 
2.3. REDUCING SATISFIABILITY OF FIRST ORDER SENTENCES TO PROPOSITIONAL ONES9 
3. Go to 1., and repeat these steps. 
Notice that if j = 0 in step 2. that is α is ∃y1β, then the Skolem function turns to be a constant function. 
If in the deﬁnition the role of universal and existential quantiﬁers are reversed, the so called existential Skolem normal form is obtained. 
Skolem normal form simpliﬁes the prenex form, however equivalence to the original formula is not true: 
Theorem 3 (Skolem normal form) 
The Skolem normal form of α is satisﬁable if and only if α is satisﬁable. 
The following deﬁnition provides a normal form for the matrix of a prenex formula. 
Deﬁnition 4 (conjunctive normal form) 
1l∨∨...1n
If a quantiﬁer free formula β is of the form (l1 where lare literals (atomic formulae or negations of an atomic formulae), β 
1 ) ∧...∧(l
m 1 
mn
∨...∨l
m 
), 
ji 
is called to be in conjunctive normal form. 
...∨l
A clause can be considered as the set of literals. 
i∨1
The disjunctions l
in
are called clause (a ﬁnite disjunction of literals). 
i 
As well as in the case of prenex normal form, for quantiﬁer free formula there is an equivalent one in conjunctive normal form. Straightforward algorithms can be constructed to generate normal forms, but we do not give the details of them. We remark that conjunctive normal forms of a formula are not unique. The concept of disjunctive normal form can be deﬁned too, where the roles of ∨ and ∧ are changed. 
If the matrix of a formula in Skolem form is rewritten into conjunctive normal form, the so called strong Skolem form is obtained. Strong Skolem form synthetises all the other normal forms. The preﬁx can be moved into the matrix because of the conjunctive nature of the matrix: 
∀xC1(x) ∧...∧∀xCm(x).	(2.1) 
A strong Skolem form can be represented by the set {C1,...Cm} of the clauses in its matrix. Here with a clause C we have to associate the universally quantiﬁed formula ∀x C. 
Notice that we can be obviously achieve that individuum variables in the 
respective clauses C1,...C
m
in 2.1 should be disjoint sets. This procedure is 
called separating the variables. 

2.3	Reducing satisﬁability of ﬁrst order sentences to propositional ones 
For semantics of propositional logic there are eﬀective ways to decide consequence relation. Moreover it is quite easy to construct algorithms to compute it on diﬀerent architectures. However most of the practical problems need ﬁrst order logic rather than propositional logic, but for ﬁrst order logic eﬀective algorithms like for propositional logic do not exist. This is why the so called Herbrand’s theorem is of great importance. Herbrand’s theorem reduces unsatisﬁability of ﬁrst order formula set to the unsatisﬁability of set of ground formulae, which can be considered propositional ones. 
Let α be a quantiﬁer free formula. A ground instance of α is a formula obtained by substituted variable free terms into the place of variables in α. The logic of ground instances is called zero order logic. Zero order logic is equivalent to propositional logic, since there is a onetoone map between the set of the ground instances of atomic formulae and the set of the predicate letters. 
The goal is: for any ﬁrst order formula set Σ to ﬁnd a zero order one Σ0 such that Σ is unsatisﬁable if and only if Σ0 is. 
Suppose that the language L does not include equality. Let α be of the Skolem form ∀x1 ...∀xmα’. Let αgj denote a ground instance of α. A version of Herbrand’s theorem is: 
Theorem 5 (Herbrand’s theorem) 
’g
∀x1 ...∀xmα’ is unsatisﬁable if and only if there are ground instances α1 ,...,α’g 
n 
g’g
of α’ such that the set {α1 ,...,αn�} is unsatisﬁable. 
It is easy to check that there is an equivalent form of Herbrand’s theorem about semantic consequence. Assume that the elements of Σ are of universal prenex forms and β is of existential prenex form. In this case Σ � β holds if and only if Σg � βg 
1 ∨ ...∨ βg holds, where Σg includes the ground instances of 
m 
the matrice of Σ, and βg runs over all the ground instance of the matrix of β or
i 
every (0 < i ≤ m). 
Herbrand’s theorem can be used to extend propositional calculi to a ﬁrst order ones this is called ,,lifting” the calculus. The simplest one is outlined below, it has completeness because of Herbrand’s theorem. 
Let Σ be a set of quantiﬁer free ﬁrst order formulas and consider the set of ground instances Σg of Σ. To prove the unsatisﬁability of Σ execute the following procedure: 
Deﬁnition 6 (DavisPutman method2) 
1. Let Ψ be a ﬁnite subset of Σg 
2. Try to prove the unsatisﬁability of Ψ by propositional logic. If it is proved, let us terminate the procedure. If not, let the new Ψ a superset of Ψ in Σg and go to step 2. 
Since propositional calculi are decision calculi, the procedure terminates, if the sets of ground instances are chosen with care (e.g. ground instances of every formula in Σ are selected in some steps). The algorithm is nondeterministic: 
2This method was introduced for resolution calculus, however it can be used for any propositional calculus. 
2.4. RESOLUTION CALCULUS 11 
the selection of the and the ground substitutions in step 2 are not determined. A search strategy is expected to deﬁne a deterministic algorithm. 
Proof procedures based on DavisPutman method were applied in theorem provers (e.g. at resolution), but they proved to be hopelessly ineﬀective. 
There is another, a more eﬀective method of lifting: using metavariables. If a human agent uses a calculus that is based on Herbrand’s theorem, (s)he has a plan and maybe a good hypothesis what term has to be used when ground instances are generated. However a search strategy of a proof procedure is almost a blind search that is why DavisPutman method is so ineﬀective. Let us recall the ∀E rule: ∀xiβ . Here t is a metavariable standing for a term of 
β[t/xi ] 
the object language. If at the execution of a proof procedure (like the DavisPutman method) it is not decided what term to be used in a step, only the ground term in the substitution is denoted by a metavariable, the procedure gets more eﬀective. Later the process of ﬁnding the proof may create constraints for the metavariables. and the proper terms can be constructed. If this method is used, the syntax has to be completed by a set of metavariables. Lifting by metavariables can be applied any propositional calculus if it is applied to ground formulae. 

2.4 Resolution calculus 
Resolution is a relatively simple calculus, but the price of this simplicity is that the calculus can be applied directly to strong Skolem normal forms only.. So strong Skolem normal form has to be constructed before starting resolution. 
We noticed in the section on normal form that every formula can be represented by a ﬁnite set of clauses using the strong Skolem form of the formula. Moreover we shall see, during the resolution procedure only clauses are used, so the procedure resolution is ,,closed,, with respect to clauses. This is the background of the terminology : resolution uses the ,,language of clauses,,. 
Resolution is a refutation calculus, we apply a kind of indirect argument that is the set Σ of premises is supplemented by the negation of the formula α to be proven, and we are going to get a contradiction. Now we survey the preparation, needed to start the proof of Σ � α using resolution calculus: 
1. Form Σ� = Σ∪{¬α}. 
2. Convert the sentences in Σ� into strong Skolem normal forms. 
3. Form the set of clauses occurring in these normal forms and separate the sets of the individuum variables occurring in them, let S the set of clauses obtained. 

Remember that a clause can be considered as a set of literals, therefore it is meaningful to speak about the clause consisting of one literal (called unit clause), and the empty clause (denoted by �) too. The empty clause is unsatisﬁable, since a clause is true in a model iﬀ there is a literal in the clause that is true in the model. Therefore � can be considered as a symbol falsity in the language. 
An important notion connected with resolution is the complementary pair of literals: an atomic formula and its negation forms a complementary pair. It is not important which element of the pair is the atomic formula therefore the notation l, ¬l is introduced for complementary pair. C \{l} will denote the clause originated from the clause C omitting the literal l from the disjunction in C. 
First we treat resolution for propositional logic. 
Deﬁnition 7 (propositional resolution rule) 
Clauses C1, C2 can be resolved if there are literals l1 ∈ C1, l2 ∈ C2 such that l1, l2 form a complementary pair3. In this case their resolvent is Res(C1, C2) is 
.
C1 \{l1}∪C2 \{l2}
Res(C1, C2) can be denoted by Resl1 ,l2 (C1, C2) too, and it is called a resolvent according to the complementary pair l1 and l2. C1, C2 are called the parents of resolvent Res(C1, C2). Clearly the resolvent of a complementary pair is the empty clause. 
It can be easily checked that {C1, C2}is satisﬁable if and only if Res(C1, C2) is. This fact implies that the resolution rule alone constitutes a sound calculus. 
Deﬁnition 8 (resolution proofs) 
A clause C can be proved from a set S of clauses by propositional resolution if there is a ﬁnite sequence C1, C2 . . . Cn = C of clauses such that for all 1 ≤i ≤n Ci ∈S or Ci = Res(Cj , Ck) for some j, k < i. 
Theorem 9 (completeness of propositional resolution) 
A set S of propositional clauses is unsatisﬁable if and only if the empty clause � can be derived by propositional resolution from S. 
Resolution incorporates several wellknown inference rules, as the following 
table shows. 	
parent clauses 	resolvent 	simulated rule 	
{P }, {¬P, Q}{P }, {¬P } 	{Q}� 	Modus Ponens: ¬elimination: chaining: 	P, P →Q �Q P, ¬P �⊥ P 	R	

{¬P, Q}, {R, ¬Q} {¬P, R}→Q, Q →R �P 
→
Now we come to ﬁrst order resolution. Resolution is deﬁne for the ﬁrst order logic where = is not a logical symbol, so the axioms of equality are not logical axioms. 
The great career of ﬁrst order resolution is due to the ﬁrst order resolution principle. A special way of lifting has been worked out for the resolution. It is known that if a pair of ﬁrst order clauses has a pair of resolvable ground instances, usually there are inﬁnitely many such pairs. The purpose is to construct such a clause as ,,ﬁrst order resolvent” that can represent as much as ground resolvents as possible maybe all of them; as the scheme below shows: 
3It is said that C1, C2 are clashing clauses or clashes on the complementary literals. 
2.4. RESOLUTION CALCULUS 
,,ﬁrst order resolution” Res1(C1, C2)
C1, C2 �−→ 
→ ↓↓
substitution substitution 
C1 g , C↓g �−→ ,,ground resolution” Resg↓(C1, C2)
2 
→ 
First some deﬁnitions connected with substitutions for the individuum variables have to be given. If p is an expression in L and σ is a substitution for some free variables, then σ applied to p will be denoted by pσ. 
Deﬁnition 10 (uniﬁer) Given two expressions p1, p2, a uniﬁer of them is a substitution σ that it makes them identical: p1σ = p2σ. If there is a uniﬁer of p1, p2, they are said to be uniﬁable. 
A natural partial ordering between substitutions can be deﬁned: σ1 is more general than σ2 if and only if there is a substitution λ such that λσ1 = σ2. 
Deﬁnition 11 (most general uniﬁer) A substitution µ is called most general uniﬁer (mgu) of expressions p1, p2 if and only if it is a uniﬁer of p1, p2, and it is the most general among the uniﬁers of p1, p2 that is for any uniﬁer σ of p1, p2 there is a substitution λ such that λµ = σ. The most general uniﬁer of p1, p2 is denoted by mgu(p1, p2). 
Theorem 12 (existence of most general uniﬁer) 
If two expressions are uniﬁable, there exists their most general uniﬁer. 
We emphasize that it is decidable whether two expressions are uniﬁable or not, moreover the most general uniﬁer is computable. 
Notice that deciding that two terms is uniﬁable means deciding that the two terms may denote the same element of Herbrand’s universe that is they have equal instances too. This fact is the basis of the following deﬁnition: 
Deﬁnition 13 (ﬁrst order complementary pair)
Literals a1 and ¬a2 constitute a ﬁrst order complementary pair if and only if
a1 and a2 are uniﬁable.

Deﬁnition 14 (ﬁrst order resolution)

Clauses C1, C2 can be resolved if and only if there are literals l1 ∈ C1, l2 ∈ C2 such that l1, l2 form a ﬁrst order complementary pair. Let µ = mgu(l1, ¬l2). Then Res(C1, C2) is (C1µ \ {l1}µ) ∪ (C2µ \ {l2}µ). 
First order resolution rule alone does not constitute a complete calculus, as the following example shows. Let us consider the clause set 
{{r(x1, x2), r(y1, y2)}, {¬r(x3, x4), ¬r(y3, y4)}}
which is clearly unsatisﬁable. However ﬁrst order resolution generates only the variants of the clause {r(x5, x6), ¬r(y5, y6)} and of the original clauses. Therefore ﬁrst order resolution has to be completed by a new rule. 
Deﬁnition 15 (factorization) 
A clause can be factorized if there are two uniﬁable literals l1,l2 in C. Then a factor of C is Cµ, where µ = mgu(l1, l2). 
Cµ can be denoted by Cl1 ,l2 and it is called a factor of C according to the literals l1 and l2.Notice that the main diﬀerence between ﬁrst order resolution and factorization is that the ﬁrst one concerns two clauses while the second one concerns only to one. 
The concept of proof for ﬁrst order resolution is analogous to propositional resolution but the clauses occurring are ﬁrst order clauses, the resolvent is ﬁrst order one and the deﬁnition must be supplemented by the condition that Ci in the proof can also be a factor of Cj for some j < i . 
The inference rules ﬁrst order resolution and factorization introduced above are called together as unrestricted binary resolution (in short binary resolution). 
Now we state the completeness theorem for ﬁrst order resolution: 
Theorem 16 (completeness of ﬁrst order resolution) 
A set S of ﬁrst order clauses with pairwise disjoint sets of individuum variables is unsatisﬁable if and only if the empty clause � can be derived by binary resolution from S. 

2.5 Automated theorem proving 
Traditionally calculus has been considered as a tool to test whether an argument is a correct proof. However with the development of computing there has emerged the demand to create programs that generates proofs, that is automatic theorem provers. The automatic theorem provers have been intended to be used in problem solving, program veriﬁcation as well as to prove mathematical theorems. 
Clearly simple procedures can be written for the inference rules they can be considered as rewriting rules too4 . However to organise these proceduresthat is the inference rules into a process that proves theorems, we have to step outside logic. The automatic theorem provers work in the same way: the consequences of the input set of sentences are generated in some order, and the program tests whether the theorem to be proved is among them. R. Kowalsky ingenuity created a conceptual frame for this situation introducing the notion of proof procedure. A proof procedure based on a proof system consists of a set of sentences, the set of inference rules and a search strategy. Clearly the sentences5 and the inference rules that generates the consequences are provided by the logic in question; these two constituents generates the consequences of the input sentences, that is the search space The search strategy is an (maybe partial) ordering over the search space: it tells that in the actual state of the 
4The eﬀect of computing is that the notion of ”rewriting” has got into the logical terminology, see [63]. 
5Morte precisely the syntax of the sentences. 
2.5. AUTOMATED THEOREM PROVING 
search space which rule has to be applied to which sentences (generated elements of the search space) with the purpose of generating new elements. 
Resolution calculus is considered as a base of automatic theorem proving, moreover it was developed for that purpose even now someone consider resolution as the calculus for theorem provers. The reason is simple: the state of art of computing technology of the sixties it was an important requirement to have a easily representable structure; moreover, having only two very simple rules helped the construction of theorem provers. However soon it has been experienced that the search space can grow to beyond control very fast this phenomena is called ,,combinatorial explosion”. Several attempts have tried to overcome it. For a decade several versions called reﬁnements of resolution have been elaborated. They constrain the growth of the search space by constraining the condition of the execution of resolution rule. Some of the variants of resolution organize the clauses into some structure like connection graphs, or into tables [15]. These variants are very eﬀective for ground clauses, however they are lifted by the DavisPutman method with metavariables which spoils eﬀectiveness. Similarly some project concentrated on the search strategy: the general results of the research in search have been applied to proof procedures. However, no adequate costfunction has been found. Several experiments have proven that there not exist ,,best” resolution proof procedure, moreover a proof procedure that provides the best eﬃciency in the case of a task, may fail to generate the proof for an other one. 
For more than two decades resolution is not the proof system generally applied in theorem proving mostly Natural Deduction and related proof systems are the base of the theorem prover systems. [18] and [70] are good introductions into the state of art of theorem provers. 
The most fruitful trend gives up automatic theorem proving and develops proof assistants. A proof assistant helps the user to describe a plan of the proof; it executes the prescribed steps and completes the proof automatically generated segments. The higher order proof assistant Isabelle is maybe the best example, a tutorial is [68], for further information visit e.g. http://isabelle.in.tum.de/. 
Chapter 3

Logic programming

The history of logic programming started with an application which was based on a resolution proof procedure, which used only so called Horn clauses and proved itself surprisingly eﬀective. First it was thought that a logic program gives a speciﬁcation of ,,what” the program is supposed to do that is it speciﬁes the inputoutput relation. However soon it was realized that using Horn clauses not only ,,what” to do is speciﬁed ,but also ,,how” to do at least in some extent. In other words: not only the inputoutput relation is speciﬁed, but an algorithm too. So there came a change of the paradigm in the application of theorem proving: to use logic as a programming language. A new slogan was announced by R. Kowalsky: 
ALGORITHM = LOGIC + CONTROL. 
The slogan expresses that the formulas of the logic programming language describe the essence of the algorithm, and the search strategy of the logic programming language ﬁlls the gaps. However the real merit of the slogan is that the segments of logic that are usable as programming language, are ideal algorithm description languages. 
For some years it was thought that the new paradigm can be expanded to the whole ﬁrst order logic, however soon it was realized that the secret of the eﬀectiveness is the restricted class of formulas. So even nowadays PROLOG and its relatives (including DATALOG) are the commonly used logic programming languages. One of the most interesting question of logic programming is which segments of logics can be considered as programming languages. This question has both theoretical and practical aspects. 
A logic programming language is a proof procedure that is a proof system and a search strategy. An axiom system is considered as a logic program, the proof of a theorem as the execution of a logic program. Since logic programming originates in problem solving, it can be supposed that the logic program consists of universal formulas and the theorem to be proved is an existential one. The theoretical condition of ,,being logic programming language” is that every proof 
17 
has to provide terms for the existentially bound variables as the result of the computation; it is explained below in details. 
Let Σ be a set of universal formulas, and let the theorem be given in the form ∃xα(x) (called goal or query). Because of Herbrand’s theorem Σ � ∃xα(x) is equivalent to Σ � α(t1) ∨ ... ∨ α(tn) for some sequences t1,...tn of terms. But, it is important to ensure this equivalence for one sequence ti only, that is to ensure the relation Σ � α(ti) for some i. The property Σ � α(ti) is called as the ,,existence of correct answer” in the logic programming community. Clearly the expectation for ,,existence of correct answer ” is a strong restriction for the segment of logic used in logical programming. 
The correct answer condition can be reformulated with the help of provability relation too: Σ � α(ti) if and only if Σ � α(ti) for a sequence ti. Terms in ti can be considered as the output of the ,,computation”. Notice that this property one of the principles of intuitionistic proof systems. 
It is more diﬃcult to formulate precisely the practical aspects of the question that which proof procedures can be considered logic as programming languages. On one hand the search for the proof has to be eﬀective, on the other hand the ,,programmer” have to have the chance to foresee the process of search for the proof. Here lies the secret of the wide spread usage of PROLOG: a logic program can be viewed and understood as a set of sentences of logic as well as a program, anticipating the execution. 
3.1 Programming with deﬁnite clauses 
Here we sketch the logical background of the programming language PROLOG and data base query language DATALOG, that is programming with deﬁnite clauses. 
Suppose that a ﬁrst order language L is given without equality. Clauses will be meant here as ﬁrst order clauses. 
Deﬁnition 17 (Horn clauses) Clauses with at most one positive literal are called Horn clauses. Clauses with precisely one positive literal are called deﬁnite Horn clauses (shortly deﬁnite clauses). 
Let the set Σ of axioms (Horn clause program) consist of deﬁnite clauses, where a deﬁnite clause may be written in the form A1 ∧ ...∧ An → B, (A1,..., An, B are atomic formulas, 0 ≤ n). Notice that n=0 is allowed, in this case the atomic formula in the implicative form is denoted by → B. 
Let the theorem (query, or goal) is ∃xα(x) where αis of the form A1 ∧...∧An (it is denoted by A1 ∧ ...∧ An → by the logic programming community). The clause form (let’s denote it β) of the negation of ∃xα(x) is obviously a negative clause. The following theorem states that correct answer problem has a positive solution for these formulas. 
Theorem 18 (existence of correct answer)
If Σ � ∃xα(x) then Σ � α(x/t) for some sequence t of terms.

3.1. PROGRAMMING WITH DEFINITE CLAUSES 
The resolution rule that is used in PROLOG is called SLD resolution (S stands for selection function, L for linear resolution, D for deﬁnite clauses1) 
Deﬁnition 19 (SLD resolution rule) 
Let Q be a negative clause in the form G1 ∧...∧Gn →, and let S be a deﬁnite clause in the form A1 ∧... ∧An → B. Q and S can be resolved if and only if literals G1, and B can be uniﬁed. Let µ = mgu(G1,B). ResSLD (Q,S)= A1µ∧...∧Anµ∧G2µ...∧Gnµ →. 
Notice the following properties of SLD: 
Two deﬁnite clauses are not allowed to be resolved. 
• 
•	The derived clauses are negative clauses, they are of the form of the goals. 
•	It is determined which literal of the negative clause has to be resolved upon. This constraint is called using selection function, it saves completeness. In traditional PROLOG systems the clauses are stored as sequences of literals, therefore the ﬁrst literal of the negative clause is selected for resolution. For this reason the ordering of literals in the derived clause is important. 

Deﬁnition 20 (SLD derivation)
Suppose that Λ is a set of deﬁnite clauses, and C is a negative Horn clause.
The SLD derivation of a clause K is a sequence �C1,...Ck � of negative Horn
clauses such that C1 = C, Ck = K and Ci is obtained as ResSLD (Ci−1,Cm) for
some Cm ∈Λ.

Let Λ and C be as in the foregoing deﬁnition. 
Theorem 21 (Completeness of SLD resolution)
Λ ∪{C} is unsatisﬁable if and only if there is a derivation of the empty clause
� by SLD resolution from the set Λ ∪{C}

There is a version of completeness that states the ,,existence of correct answer ”. Let Σ and ∃xα(x) the same formula set and formula as in Theorem18, and let Λ be the clause set corresponding to S =Σ ∪ {¬α(x)}, and let us suppose that the empty clause can be derived from S by SLD resolution. Let σji be denote the most general uniﬁcation applied to xj in the ith step of the derivation. 
Corollary 22 ( existence of correct answer)
Let us consider terms tj = xj σj 1 ...σjn, where n is the length of the derivation.
Then t = �t1,...tm� is a correct answer, that is Σ � α(ti).

1For general clauses one of the most eﬀective reﬁnement of resolution is the so called SL resolution (linear resolution with selection function). However the secret of the SL resolution is the elegant and eﬀective way how it executes the resolution steps between two derived clauses and this step does not occurs in the case of deﬁnite clauses, so in this case SL turns to be input resolution with selection function. 
For deﬁnite clauses a so called ,,procedural semantics” was provided: a deﬁnite clause is a procedure with B as the head and A1 ∧...∧ An as the body. Each Ai calls procedures whose head can be uniﬁed with Ai. In this interpretation ,,calling a procedure” corresponds to an execution of SLD resolution inference rule. 
Let us see a simple example. In logic programs we often use data type list that is the language has a constant ,,nil” for empty list, and a binary function ,,.” for list constructing operation. The logic programs act over the Herbrand’s universe generated by them that is they act over lists. The following simple program deﬁnes the ,,element of a list” relation (small case letters denote constants and upper case letters denote variables): 
Element(X, L.X)←
Element(X, L.Y)←Element(X, L) saying that ,,X is element of a list if it is the head of the list, or if it is the element the tail of the list”. 
Notice that the same program can be used for diﬀerent aims. The goal Element(a,l) tests whether a is an element of l, Element(X,l) takes an element of l (the head if the search strategy is considered too), Element(a,Y) creates a partially deﬁned list with a as an element (as head). 
If procedural semantics is considered then it can be said that a sophisticated calling mechanism is used for the parameters: the same parameter can be input or output one depending on the call of the procedure. It is called ,,call by need”. 
Further interesting properties of logic programming languages are 
• there are no iteration in them, only recursive algorithms can be written, 
• there is no assignment statement only bounding of variables. 

Clearly the search space of SLD resolution can be considered as a tree, where the branches are derivations. So the problem of the search for the answer (for the empty clause) is transparent. So the search for the solution is built into the interpreters. In PROLOGlike logic programming languages the depth ﬁrst search strategy is used, therefore calling of procedures (execution of resolution steps) can be backtracked. 
These features soon have been built into other programming languages too. 
The most important features of the paradigm ,,programming with Horn clauses” can be summarized as follows2: 
1. The existence of a single intended model (the least Herbrand’s model) yields the semantics for Horn clause programs and ensures the existence of correct answer. 
2. The Herbrand’s universe allows the programmer to use function symbols in the language as constructors of abstract data types, to encode objects as terms and to represent recursive deﬁnitions of these objects by means of Horn clauses. 

2Based on[62]. 

3.2. ON DEFINABILITY 21 
3. Horn programs can specify any recursively enumerable set, so programming with Horn clauses captures the commonly accepted notion of computability. 
4. Programming with Horn clauses is declarative due to the separation of logic, represented by sets of Horn clauses, from uniform control, represented by SLD resolution. 

3.2 On deﬁnability 
To understand the theoretical base of logic programming ﬁrst we summarize some aspects of the theory of deﬁnability. Deﬁnability has an extensive theory inside logic. We deal only with a special part of it, with the theory of inductive deﬁnitions. This topic is particularly important in applications. 
Let L be a ﬁrst order language, and let R be a new kary relational symbol. Let L� be the language obtained from L by expanding it with R. The models of � are denoted by �M, R��, where M is a model of L and R’ is the interpretation 
L
of M. 
We remark that here only the case of one symbol R is discussed for the sake of simplicity. But everything what is said in this section is true for simultaneous introduction of more than one relational symbols. 
Deﬁnition 23 (diﬀerent forms of deﬁnitions) A sentence of the form ∀x(R(x) ↔ α(x)) is called an explicit deﬁnition of R, if α(x) is a formula of L (that is it does not contain R). A set of formulae ΣR consisting of formulae of L� including relational symbol R is called the implicit deﬁnition of R. If for a model M of L and relation R� it holds that �M, R�� � ΣR then it is said that ΣR deﬁnes R� in M. If R�is the only interpretation of R such that it satisﬁes ΔR, it is said that ΣR uniquely deﬁnes R�in M. A sentence ΔR of the form ∀x(R(x) ↔ α(x, R)) is called the inductive deﬁnition of R, if α(x, R) is a formula of L�. α is called the deﬁning formula of the deﬁnition3 . 
The basic question of deﬁnability theory is that what kind of deﬁnition can uniquely deﬁne a relation. Clearly an explicit deﬁnition uniquely deﬁne the relation in question, since the deﬁning formula deﬁnes a well determined relation in every model of L. As regards implicit deﬁnitions see the following theorem: 
Theorem 24 (deﬁnability)
Suppose that an implicit deﬁnition ΣR uniquely deﬁnes a relation on each model
of L. Then there is an explicit deﬁnition of the relation.

3Note that if ΔR deﬁnes R� in �M, R��, then the truth set of the deﬁning formula in �M, R�
provides prescisely R�. 
Clearly inductive deﬁnitions are ,,implicit deﬁnitions” of special form. The theorem implies that inductive deﬁnitions themselves are very weak concepts, this is why they are further analyzed below. If ﬁrst order logic is considered, its expressive power is not greater than that of implicit deﬁnition. However in the theory of inductive deﬁnition strong results can be found (for the theory of inductive deﬁnability see [7]) 
Deﬁnition 25 (least ﬁxed point of an inductive deﬁnition on a model) 
Let M be a model of Land �
R be a relation deﬁned by ΔR = x(R(x) ↔α(x,R)).
∀
R is the least ﬁxedpoint of ΔR, if for any R’ deﬁned by ΔR it holds that �
R ⊆
R’4 . 
It can be proven that in general the least ﬁxed point of an inductive deﬁnition can not be deﬁned uniquely in ﬁrst order logic. The deﬁning formula α(x,R) can be considered as a set theoretically operator in algebraic logic. As regards the terminology ,,least ﬁxed point,, of an inductive deﬁnition, it is the same as the least ﬁxed point of the set theoretical operator associated to the deﬁning formula. 
Some inductive deﬁnitions do not deﬁne relations at all (simplest example: 
R(x)); or even if there are deﬁned relations on M, there are no least 
R(x) ↔¬
one (simplest example: R1(x) ↔¬R2(x), R2(x) ↔¬R1(x)). 
Deﬁnition 26 (PE deﬁnition) 
If relation symbol R occurs only positively in a disjunctive normal form of the
deﬁning formula α, then the deﬁnition ΔR is said to be positive. If universal
quantiﬁer does not occur in some prenex form of α then the deﬁnition ΔR is said
to be existential. The positive existential deﬁnitions are called PE deﬁnitions.

Theorem 27 (existence of least ﬁxed point)
For any model M positive deﬁnitions have a least ﬁxed point, positive existential
deﬁnitions have a recursively enumerable least ﬁxed point.

The construction providing the least ﬁxed point for ΔR in terms of a sequence of relations on M is deﬁned as follows: 
R0 = ∅ 
R1 = {q �M,R0�� α(q)}
|
. 
. 
.
Rn+1 = {q |�M,Rn�� α(q)}

Theorem 28 (construction of least ﬁxed point)
If ΔR is a PE deﬁnition then ∪n<ω Rn is the least ﬁxed point of ΔR in a model

M. 
4Relation�
R is the least one in the set of deﬁned relations according to the ordering ⊆ (set theoretical inclusion). 
3.3. GENERAL PARADIGM OF LOGIC PROGRAMMING 23 
This construction has a more general form too: if any set of ktuples is taken as R0, the construction provides the least ﬁxed point that includes R0. 
For positive deﬁnitions there exists a so called greatest ﬁxed point too, and for positive universal deﬁnitions the complementer set of the greatest ﬁxed point is recursively enumerable. 
Inductive deﬁnability is applied in several ﬁelds of Computer Science, therefore some logics are deﬁned with built in ﬁxed point operators, that is in these logics there is a logical symbol, e.g. fxd for the least ﬁxed point. In the deﬁnition of the syntax the condition ,,if α is a formula then fxd α is a formula” is inserted. The meaning of a formula fxdα is the least ﬁxed point of the deﬁnition ∀(R ↔ α) where ∀ means universal closure. Clearly this operator leads out of ﬁrst order logic, since in several cases the least ﬁxed point can not be explicitly deﬁned. 
Here is an example: the least ﬁxed point of deﬁnition 
R(x) ↔(x = 0 ∨∃y(x = s(y) ∧R(y))) is the set of natural numbers in every model of the Peano axioms, but it can not be deﬁned in ﬁrst order logic. 
About ﬁxed point logics see [20]. 

3.3 General paradigm of logic programming 
Since the meaning of a program can be considered as the inputoutput relation, the general form of logic programs can be searched in the form of deﬁnitions. 
The existence of least ﬁxed point ensures the fulﬁllment of the existence of correct answer therefore positive inductive deﬁnitions are the adequate candidates for logic programs. Since the answer must also be computable, positive existential (PE) deﬁnitions can be considered as logic programs. More precisely a logic program is a set of PE deﬁnitions; however every result for one deﬁnition holds for sets of deﬁnitions too. Any kind of calculus can be joined to the class of PE deﬁnitions, the special syntax turns them quite similar. 
It is shown below how we obtain a deﬁnite clause program from a PE deﬁnition if resolution is wanted to be used. For resolution the deﬁnition has to be transformed into clausal form. 
Let ΔR = x(R(x) ↔α(x,R)) be a PE deﬁnition. For the ﬁrst step of the 
∀
transformation the following theorem is needed: 
Theorem 29 (about least ﬁxed point)
There exists the least relation satisfying formula ∀x(R(x) ← α(x∧,R)), and it
is the same as the least ﬁxed point of ∀x(R(x) ↔α(x,R)).

So if we are only interested in the least ﬁxed point, Δ can be substituted by x(R(x) ←α(x,R)). Let us execute the following transformations: 
∀
x(R(x) ←α(x,R))
∀
if and only if
x(R(x) ←∃y(α1(x,y,R) ∨...∨αn(x,y,R))

∀
where αi(x,y) is a conjunction for every 1 ≤i ≤n 
if and only if
x∀y(R(x) ←α1(x,y,R)) ∨...∨αn(x,y,R))

∀
if and only if x∀y(R(x) ←α1(x,y,R))∧ ...∧∀x∀y(R(x) ←αn(x,y,R))∀which can be written as a set of Horn clauses x∀y(R(x) ←α1(x,y,R), ...∀x∀y(R(x) ←αn(x,y,R))}
{∀
Finally, if there are atoms of the form x = t in a conjunction αi(x,y,R), let us substitute x by t in the conjunction. In this way a deﬁnite Horn clause program is obtained. 
Let us consider the program deﬁning the ,,element of a list” relation, which was given above. It can be gained from the deﬁnition 
∀X,YElement(X,Y)↔∃T(Y=T.X) ∨∃Z,T(Y=T.Z∧Element(X,T)). 
The transformation into deﬁnite clause program: ∀X,Y(Element(X,Y) ←(∃T(Y=T.X) ∨ ∃Z,T(Y=T.Z∧Element(X,T)))) iﬀ ∀X,Y(Element(X,Y) ←∃Z,T(Y=T.X ∨ (Y=T.Z∧Element(X,T)))) iﬀ ∀X,Y,T,Z(Element(X,Y) ← (Y=T.X ∨ (Y=T.Z∧Element(X,T)))) iﬀ ∀X,Y,T(Element(X,Y)←Y=T.X)∧ ∀X,Y,Z,T(Element(X,Y)←(Y=T.Z∧Element(X,Y))) 
Written as Horn clause program: Element(X,T.X), Element(X,T.Z)←Element(X,T) 
The selection of other calculi than SLD resolution, may result a logic programming language diﬀerent from the languages based on resolution, see [80]. 
It is the user’s free choice what he/she considers a logic program: the implicative sentences (the sets of deﬁnite clauses) or the deﬁnition with equivalence (completed deﬁnition of the deﬁnite clause program). 

3.4 Problems and trends 
One of the most controversial questions of logic programming was the question of negation, which is in fact two questions: 
1. How to infer negative information from a deﬁnite program? 
2. How negative literals can be used in logic programs? 

If we want to answer the ﬁrst question, ﬁrst a decision has to be done: when a negative literal is considered the consequence of a logic program. There are three alternative answers: 
1.	If a tupple q does not belong to the least ﬁxed point, then ¬R(x)[q] holds. In this case the logic program is considered with implication instead of equivalence. Clearly if the least ﬁxed point is not recursive, there is no complete calculus for negation. Sometimes this condition is called closed world assumption in the context of data bases. 
3.4. PROBLEMS AND TRENDS 
2.	If a tupple q does not belong to the greatest ﬁxed point, then ¬R(x)[q] holds. This answer is adequate for the inductive deﬁnability approach. There is no complete calculus for this case, since the complementer set of the greatest ﬁxed point of a PE deﬁnition may not be recursively enumerable. In this case the tupples can be partitioned into three sets: the least ﬁxed point, the complementary set of the greatest ﬁxed point, and the diﬀerence between the greatest and the least ﬁxed points. This fact suggests that an adequate semantics can be deﬁned based on three valued logic it is done in [23]. 
3.	A negative literal holds if it is the semantic consequence of the completed deﬁnition of the logic program. This answer takes into consideration the whole class of models, therefore it is not adequate for the inductive definition approach. However we have complete inference rule only for this solution: the so called negation as failure. Negation as failure was introduced for deﬁnite clause programs; it says that the negative literal holds if the positive cannot be proved from the logic program (set of Horn clauses). Negation as failure was criticized as a ,,non logical” method, however soon the completeness was proved. Moreover, if Natural Deduction is applied to PE deﬁnitions to prove a negative literal (starting from the ,,¬ introduction rule,,) the structure of the proof corresponds precisely to the negation as failure method. 

Notice that an answer for the ﬁrst question does not works the second one. If negative literals occur in the deﬁning formula, the existence of the least ﬁxed point cannot be ensured. There were several trials to interpret a deﬁned relation as the meaning of the nonpositive deﬁnition (see e.g. [12]): the generally known approaches are the stratiﬁed programs, stable semantics and well founded semantics based on three valued semantics [84]. [35] proposes an interesting kind of logic program, the so called quasi equations. A quasi equation consists of the separate deﬁnitions of the positive and the negative literals: R(x) ← ρ1(x), ¬R(x) ← ρ2(x). 
A logic programming language is a proof procedure, therefore the PE deﬁnitions as programs and the selected calculus have to be completed by a search strategy. The problem of search strategy is presented here for deﬁnite clause programs. Because of the restricted set of formulas used in the proofs the search space turns to be of a tree structure, precisely an andor tree. There are two questions to be decided by a search strategy: 
1. If a goal is given in the form of A1 ∧ ...∧ An →, it has to be decided which literal Ai has to be eliminated ﬁrst (which has to be resolved upon). The node in the search tree corresponding to this decision is an and node, since all the literals has to be eliminated. In the traditional deﬁnition of PROLOG the goals as well as all the clauses are represented as sequences of literals, and the ﬁrst literal is selected. 
2. For a selected literal a deﬁnite clause has to be selected, which can be resolved upon the literal. This selection is represented by an or node. 
In the traditional deﬁnition of PROLOG the and nodes do not occur in the search tree, since the selection function determines the literal to be eliminated. So an or tree is obtained. The deﬁnite clauses with the same relation symbol in their heads5 are ordered, and they are selected in this order. The search strategy is depth ﬁrst traversing of the search tree. Notice that this search may lead the execution into an inﬁnite branch even the empty clause can be generated, so spoiling completeness. However, the programmers can inﬂuence the process of the search by the order of clauses and the order of literals in the clauses so it is the programmer’s responsibility to write programs which do not loop6 
Below we outline some of the important trends of logic programming. 
•	The fact that the logic program interpreters (compilers) are based on search suggests the application of parallel execution. In that case the andor tree representation is adequate. Two kinds of parallelism are distinguished: if branches coming from an and node are traversed parallel, we speak about andparallelism; if branches coming from an or node are traversed parallel, we speak about orparallelism. While the orparallelism does not raise theoretical problems, andparallelism does so. The diﬃculty is that literals in a goal may contain the same variable. The two occurrences have to bind by the same way, so the two branch cannot be traversed independently of each other. 
•	,,Pure”7 logic programming is applicable to computation on abstract data types constituting a Herbrand’s universe. However, abstract data types and data types, where real computation occurs (e.g. numbers), are mostly used together. Even in the ﬁrst variants of PROLOG there were so called ,,built in” predicates evaluating arithmetic expressions. Constraint logic programming expands this feature, where equations and inequalities are collected while proving the goal, and when there are no literal to be eliminated by the inference rules, the system of the collected equations and inequalities is solved by mathematical methods. 
•	With the development of the ﬁeld of knowledge based systems new types of reasoning, diﬀerent from deduction, were applied, like abduction and induction. Soon the logic programming languages corresponding to them have appeared: 

Abductive logic programming is an expansion of the traditional one. Beside the logic program a set of atomic formulas is given, which can be taken 
5They form a ”partition” in the PROLOG terminology.
6Moreover commands to eﬀect search are included in PROLOG.
7A logic program is pure if every step of the execution is executed by an inference rule.

3.4. PROBLEMS AND TRENDS 
as hypothesis. If the deduction fails, some of these atoms can be used as input clauses to continue the derivation. Then the result has to be understood ,,assuming hypotheses ...”. About the application of abductive logic programming see e.g. [53]. 
Inductive logic programming” is concerned with the development of inductive learning algorithms that use ﬁrst order deﬁnite clause logic as the knowledge representation” this is how the Introduction of [67] deﬁnes the ﬁeld. Inductive logic programming reverses the task of logic programming: positive and negative examples are given, and a logic program has to be synthesized which computes all the positive examples and none of the negative ones. Background knowledge in the form of deﬁnite clauses can help induction. Inductive logic programming can be used in knowledge extraction (data mining) as well as in optimizing logic programs. For a detailed discussion see [66]. 
In the last tenﬁfteen years a new paradigm of logic programming has been evolved, which diﬀers from Horn logic programming in several important aspects therefore it is worthwhile to discuss it in a more detailed way. The origin of this trend was the problem of negation. If negated atoms are used in the body of a Horn clause, the may not have a least model only several minimal ones. Research in this direction ﬁrst tried to select one of them as ,,intended” model, but without signiﬁcant results. The great change came when the stable model semantics was introduced: let us consider not one intended model, but a family of ,,intended” models. From this decision a new variant of logic programming called stable logic programming (SLP, for short), or answer set programming has been born. 
However, if function symbols are used as in Horn logic programming (allowing to express any partial recursive function by its recursive deﬁnition) and several ,,intended” models are considered, then the executions of logic programs increases well beyond acceptable notions of computability. Therefore in SLP function symbols cannot be used, thus syntax is the same as the syntax of DATALOG. Note that in this case the Herbrand’s universe is ﬁnite, the set of ground atoms (Herbrand’s base, as it is called in the logic programming community) is ﬁnite. Therefore the ﬁrst order logic of that language can be transformed into propositional logic. 
The stable models of a logic program can be understood as follows. Let P be a logic program, and let be Pg be the set of the ground instances of clauses in P . For the sake of simplicity we identify models with their positive diagrams, that is with the set of positive ground atoms. Let M be such a set, it is called a stable model of P if M coincides with the least model of the reduct P M of Pg
g 
with respect to M . It is obtained from Pg in two steps: 
• for every ground atom p ∈ M all the clauses containing not(p) are omitted, 
• from the body of every remaining clause the negative literals are omitted. 

Clearly M is a model of P too. Stable models have several ,,nice” properties, which we cannot explain here these are deﬁned and discussed in the literature about diﬀerent theories about negation in logic programming. However, we mention that the deﬁnition of stable models as the other constructions in this ﬁeld is greatly inspired by the developments in the ﬁeld nonmonotone logics, which we discuss later. [[62]] is an easy and interesting introduction into stable logic programming, is recommended to the interested reader. 
SLP is a basically diﬀerent paradigm from the traditional Horn logic programming from the point of view of programmers too. While traditionally the result of a computation is a term (or some terms), in the answer set programming the result are sets of atomic statements (facts). An example: traditionally a path in a graph is expressed as a list of edges, while in answer set programming a set of edges. In the traditional case the result holds in every intended model (the term belongs to every ﬁxed point of the deﬁnition), in answer set programming diﬀerent results are supplied for diﬀerent intended models. 
Software implementations to compute answer sets are DeReS, dlv, NoMoRe, smodels;.to get some information about them visit www.cs.unipotsdam.de. 
Chapter 4

Program veriﬁcation and speciﬁcation 
4.1 General introduction 
Software industry has a very dubious character, since there is no reliable quality control for its products. This was the origin of the so called ,,software crisis” at the beginnings of sixties. Since then software engineering has developed several software technologies to overcome the crisis. 
The idea to use logic for veriﬁcation of programs exists parallel to the problem of quality control. To discuss the diﬀerent logic based approaches ﬁrst the meanings of programs have to be clariﬁed and to overview the program properties that can be investigated by logics. 
The data types are interpreted in relational structures (e.g. in many sorted models). The so called state transition semantics is considered. The simplest notion of state is an evaluation of program variables. Statements of the programming language as well as programs are considered state transitions.A state transition is deﬁned as the set of pairs of input and output states. So the meaning of a program is the set of pairs �qi,qo� such that there is an execution with output qo for input qi. This set is called the inputoutput relation of the program. Clearly the inputoutput relation is a partial function in the case of deterministic programs. The sequence of states of an execution called trace is sometimes considered as the meaning of the program. 
The most apparent program properties are correctness and termination, however the concept of correctness has to be clariﬁed. Correctness can be deﬁned with respect to (w.r.t.) a speciﬁcation expressed by a pair of formulas �ϕ(x),ψ(x)�. Formula ϕ(x), called precondition, constraints the input state of the program, and ψ(x), called postcondition, speciﬁes the output state. Notice that while these two conditions contain the same variables, they refer to diﬀerent evaluations. While a pair of preand postconditions may specify the program execution partially, the weakest precondition and strongest postcondition can be 
29 
considered as the total speciﬁcation of the program. 
Let p be a (non deterministic) program, ϕand ψ beﬁrst order formulas. The following deﬁnitions give the meaning of some generally used program properties. 
Deﬁnition 30 (safety (invariance) properties)
The safety (invariance) properties express that a ,,good property” is always true.
Some of the important ones:

•	,,a program p is partially correct w.r.t.�ϕ(x),ψ(x)�” means that ,,if the input state satisﬁes condition ϕ(x), each output state of p satisﬁes condition ψ(x)”; 
•	,,program p has invariant ψ(x) at a point of the program w.r.t precondition ϕ(x)” means that ,,if the input state satisﬁes condition ϕ(x),condition ψ(x) holds when any execution of p reaches the point marked by the invariant”. 

Deﬁnition 31 ( liveliness (eventually) properties)
The liveliness (eventually) properties express that a ,,good property” eventually
happens. Some of the important ones:

•	,,program p quasiterminates w.r.t precondition ϕ(x)” means that ,,if the input satisﬁes condition ϕ(x), program p has a terminating execution path”; 
•	,,program p terminates w.r.t precondition ϕ(x)” means that ,,if the input satisﬁes condition ϕ(x), every execution path of program p terminates”; 
•	,,program p is quasitotally correct w.r.t. �ϕ(x),ψ(x)� ” means that ,,if input satisﬁes condition ϕ(x), program p has an output state satisfying condition ψ(x)”; 
•	,,program p is totally correct w.r.t. �ϕ(x),ψ(x)� ” means that ,,if input satisﬁes condition ϕ(x), every output state of program p satisﬁes condition ψ(x)”. 

The traditional notation for partial correctness is {ϕ}p{ψ}, for total correctness is [ϕ]p[ψ]. 
Theoretical computing science usually consider some metalanguage as programming language. It it contains some kind of iteration, its precise form does not count: the theoretical results do not depend on the detailed syntax. In the deﬁnitions nondeterministic programs are supposed, which have welldeﬁned starting point and termination. In the case of deterministic programs the notions ,,quasiterminating” and ,,terminating” coincide; similarly, the notions ,,quasitotally correctness” and ,,totally correctness” coincide. Notice that termination can be expressed in terms of total correctness with true as postcondition; further, looping can be expressed by partial correctness with postcondition false. In the case of a program which fulﬁlls its function continuously 
4.2. FORMAL THEORIES	31 
(like operation systems, word processors etc.), the state of termination is not characteristic. In that cases the postcondition can be aﬃxed to any point of the program. 
Naturally there are many other interesting program properties that can be investigated by logic. For example whether a parallel (or cooperative) program is deadlockfree. Recently almost any program property is discussed in terms of logic except for performance properties. As an example we refer to [52], which studies the formal handling of ,,secure information ﬂow”. Nowadays the multiagent technology raises the problem of spatially distributed computation. In this case we have to be able to express statements like ,,there is a process at location n, which is able to satisfy speciﬁcation σ”. The interested reader has to visit website research.microsoft.com. 
In the following we outlines the theoretical base of program veriﬁcation. All the statements are independent of the precise syntax of the programming language; only we have to suppose that some form of iteration is included. In the traditional research ,,while language” is used. Variants of state transition semantics are considered as the semantics of the programming language. 
First [24] proposed a method to prove partial correctness, his method was formalized as a calculus by [48]. The method basically is an induction on the structure of the program. The FloydHoare calculus consists of inference rules corresponding to the program constructions. Let us see two examples, the introduction rules for the sequence of statements and for while statement. 
{ϕ}p1{λ} , {λ}p2{ψ} 
; I	(4.1) 
{ϕ}p1;p2{ψ} 
ψ , ϕ ∧α →λ , {λ}p{λ} , ψ
ϕ ∧¬α →	λ ∧¬α →while I 
{ϕ} while α do p od {ψ} 
(4.2) 
Note that in both cases an invariant assertion (denoted by λ) is used for the decomposition of the program construction in question. In the ﬁrst case the invariant can be generated automatically; however, to ﬁnd a suitable invariant for loops needs human intuition, that is understanding the program. 

4.2 Formal theories 
To formalize computing has been a great challenge for logic. There are several approaches, let us list some of them: 
•	Relation algebras and its logics are widely used, since relations can be considered as meanings of programs. 
•	New logics are deﬁned for modelling computing. New connectives are deﬁned as in linear logic (see [40]), or semantics is modiﬁed as in dynamic predicate logic1 (see e.g. [42]). The most known one is dynamic logic, which is discussed below. 
•	Nonclassical logics are used e.g. intensional logic or diﬀerent temporal logics (discussed below). 
•	Even ﬁrst order classical logic can be used a version is discussed below. 

Naturally the most important problem is the completeness of the proof system to be used. The problem can be raised independently on the logic in question. It seems that any proof system proving partial correctness cannot be complete, since looping can be expressed as partial correctness and it is known that termination is an undecidable problem. It is strange that it was not realized while methods to prove program properties were developed. The reason is that a special notion of completeness was investigated. The ﬁrst results of noncompleteness were developed in the late seventies, see [34] and [85]. There were several trials to cope with it, e.g. the notion of arithmetical completeness was used to characterize computational logics. Arithmetical completeness compares a computational logic to the logic of arithmetics: it means that the logic in question would be complete if arithmetics was. 
The real solution for the problem of completeness was given by the Hungarian school, namely [9] creating a complete computational logic, by modifying of the notion of termination. This will be discussed in the subsection below about ﬁrst order programming theory. 
Deﬁnability may play also an important role in programming theories, however we do not have space enough to discuss it. 
4.2.1 Dynamic logic 
Dynamic logic was developed in the late seventies; [45] is a good summary. 
Dynamic logic is a multimodal logic, where modal operators are labelled by programs. It means that classical logics are extended by modal operators [p] as box operator and �p� as caro operator, where p denotes a program. Notice that programs are deﬁned by grammar too, so diﬀerent programming languages have diﬀerent dynamic logics. However the properties of diﬀerent dynamic logics do not diﬀer. Generally nondeterministic programming language is considered, and a meta language armed with test statement and iteration is deﬁned as programming language. Here we outline dynamic logics it was deﬁned by Harel and his coworkers, however now new logics are based on traditional dynamic logic, e.g. mucalculus combines dynamic logic with ﬁxedpoint operator. 
1Interesting that the semantical approach behind this logic originates in modelling of computing, however it is used in linguistics rather than in computing. In spite of the similar name, dynamic predicate logic and dynamic logic are two basically diﬀerent logics. 

4.2. FORMAL THEORIES 
In the semantics of dynamic logic the set of worlds is the set of states and the accessibility relation is represented by the executions of the program in question. For every world the same structure is rendered, which represents the data types of the programming language in question. 
To get the deﬁnition of the meaning function of ﬁrst order dynamic logic, that of classical ﬁrst order logic has to be completed as follows. 
Deﬁnition 32 (meaning of dynamic modal operators)
Let Pp denote the inputoutput relation of p. The truth set of [p] α is the set:

�q, a� belongs to Pp for any evaluation a ∈[α]},
{q |
the truth set of �p�α is the set: �q, a� belongs to Pp for some evaluation a ∈[α]},
{q |
Remember that q ∈[α] denotes that q is included in the truth set of α. 
Intuitively [p] α says that α is true after any execution path of p, and �p�α says that there is an execution of p such that α is true after it2 . Note that he truth set of the formulae are the set of inputs. We deﬁned ﬁrst order dynamic logic, however propositional one is important too. 
The important program properties can be expressed in dynamic logic as 
follows: 
program p is partially correct w.r.t. �ϕ, ψ� ϕ [p]ψ 
program p is quasitotally correct w.r.t. �ϕ, ψ�→
ϕ → �p�ψ 
program p quasiterminates w.r.t. precondition ϕϕ → �p�true. 
For deterministic programs total correctness is the same as quasitotally correctness, however for nondeterministic programs it is complicated to construct the formula expressing total correctness. 
The inference rules (4.1) and (4.2) can be expressed by dynamic logic axioms: ((ϕ →[p1]λ) ∧(λ →[p2]ψ)) →(ϕ [p1; p2]ψ), 
ψ) ∧(ϕ ∧αλ) ∧(λ→
→[p]λ) ∧(λ ∧¬α →ψ)) →(ϕ 
((ϕ ∧¬α →[while α do p →od] ψ)
→
respectively. Clearly these axioms can be expressed as inference rules too. 
Theorem 33 (compactness and completeness) 
Propositional as well as ﬁrst order dynamic logics are not compact. Propositional dynamic logic is weakly complete, but it is not strongly complete. First order dynamic logic is not weakly complete. 
The theorem above holds for the traditional interpretation of termination; however the negative results can be turned into positive, as it will be shown in the discussion of ﬁrst order logic with explicit time below. 
Notice that dynamic logic is adequate also to model any processes if they can be decomposed into elementary subprocesses. 
2Remember that non deterministic programs are discussed. 
4.2.2 Temporal logic 
Temporal logic was ﬁrst used in [73] to characterize a method of proving program properties. From that time temporal logic is widely used, mainly for parallel programs. 
Temporal logic applied for programming uses other temporal operators than the standard ones described in [22]. The modalities referring to the past are superﬂuous. The time scale is a discrete ordering, representing the steps of the execution of a program. To handle such a timescale new operators are introduced. Diﬀerent approaches may use diﬀerent operators, e.g. [73] introduces modality ,,until”, [37] uses modalities 1 with the meaning ,,it is true in the ﬁrst moment” and next with the meaning ,,it is true in the next time moment”. 
Generally, if temporal logic describes computation, the programs do not appear explicitly in the language. For a program a set of axioms is generated, which describe the possible traces. We do not have space enough here to detail how to perform it. Non rigid constants correspond to program variables, while rigid variables are used in the formulas describing properties of states. The history of a program variable can be obtained by a function that maps the time scale to the evaluations of a constant representing the program variable3 . However, [?] adds ,,actions” to his time logic (TLA), which has been developed into a practical specifying language below we discuss it. In TLA actions are introduced directly, it makes the descriptions of the program executions easier and nearer to intuition. Curiosity of the logic is that actions are formulae at the same time: an action is true in a time structure if it transmits the ﬁrst state into the second one. 
In propositional case temporal computational logic can be embedded into dynamic logic, that is any temporal formula can be expressed by a dynamic formula. However [37] proves that the two ﬁrst order logics cannot be compared: there is a temporal formula that cannot be expressed in dynamic logic, and a dynamic formula that cannot be expressed in temporal logic. 
Traditionally, temporal logic uses the ordered set of natural numbers as time scale, and therefore it is not complete in the ﬁrst order case. [56] provides a comprehensive overview of the result of the traditional approach. If the time scale belongs to a more general class (like the class of sets with discrete ordering and successor and precedessor functions), a complete temporal logic can be developed. [10] provides a survey of temporal logics with general time scales used for programming theories. 

4.2.3 First order logic with explicit time 
First order logic with explicit time can be used to characterize program execution. It can be considered as a translation of temporal logic into ﬁrst order one. It was published ﬁrst in [36], a detailed discussion can be found in [37]. 
3In intensional logic such functions can be referred in the language, they form the ”intensions” of the constants. 

4.2. FORMAL THEORIES 
For the sake of simple presentation we use a many sorted logic. Beside data type sorts additional sorts are supposed: 
•	time sort (t), corresponding to the time scale of temporal logic, 
•	function sorts4 (dt) for any data sort d, representing the history of a program variable of sort d in the execution, so they stand for functions mapping time to data. 

The language has to be completed with additional nonlogical symbols to handle time (e.g. constant 0 for starting moment, function s with the meaning ,,next”, and the predicate <). For any data sort d function symbol appd with arity �t, dt; d� is added to the language, that is its interpretation in a model is a function that tells us what is the value of the function in a given moment. Let us denote the set of sentences of the completed language by Ft. 
Axioms are needed to ensure that in every model the interpretations of the additional symbols reﬂect the intuitive meanings. These axioms belong in the following three groups, where t denotes a time variable, f and g denote function variables: 
•	axioms for time, describing a discrete ordering, 
•	induction axiom scheme for time: (α(0) ∧∀x(α(x) →α(s(x)))) →∀xα(x), 

axioms for function sort: 
• 
–	axioms for equality: ∀t appd(f, t) = appd(g, t) →f = g for every data sort d; 
–	diﬀerent versions of comprehension scheme expressing that there are as many elements of function sort as we need, that is e.g. for every deﬁnable function there exists an element of the function sort: 

t∃!yα(t, y) →∃f∀tα(t,appd(f, t)).
∀
Models satisfying these axioms are called models with inner time, let us denote this class by Mt. A model is called a standard model if the time sort is isomorphic with natural numbers. Let Ms denote the class of standard models. 
t 
Logic �Ft, Mts, m�is called the standard time logic, �Ft, Mt, m�is called the time logic. 
In standard time logic the interpretation of termination is the traditional one: the program stops in ﬁnitely many steps. However in time models the program may stop at a non standard moment. To characterize the traces in non standard moments the description of the program has to be completed by an induction axiom, saying that 
if ,,a property is true at the starting point”, and ,,if this property is true in a moment, it remains true in the next moment” then ,,this property is true in every time moment”. 
4Some authors use the terms path or intension. 
Theorem 34 (completeness) 
Standard time logic is not complete, time logic is strongly complete. 
In time logic it is clear why traditional programming logics are not complete. While data are considered as any model of the axiom system in question, time is supposed to be a standard model, which cannot be axiomatized. The interpretation of termination spoils completeness even in the case of logics where time does not appear explicitly. If also nonstandard time scales are considered, completeness is ensured. First [9] realized this. Induction axiom for traces can be expressed in dynamic logic as well as in temporal one, so complete versions of these logics can also be created see [37]. 
Clearly temporal logic can be transformed into time logic, this can be proved about dynamic logic too. 

4.3 Logic based software technologies 
The analysis of programs by logical means ﬁrst aimed to prove the properties existing programs. However soon the paradigm has changed: the aim has become to write correct programs, and logic based software development technologies have been developed to this aim. Technologies follow a topdown development strategy and may consist of 
•	speciﬁcation language, which supports to specify software products in several levels, 
•	methods to prove that reﬁnements of the speciﬁcations are correct, 
•	methods to generate code for the speciﬁcation. 

Speciﬁcation languages are generally based on logic. Note that pure logic cannot be used, because 
•	a speciﬁcation has to be structured that is some kinds of units are needed, which can refer one to another but logic studies only sets of sentences, no other structure; 
•	the type structure of programming language has to be represented in the logic used for speciﬁcation; 
•	the speciﬁcation speaks about higher order objects (e.g. functions) constructions to deﬁne such objects has to be provided for the speciﬁcation language. 

[60] illustrates how a speciﬁcation language is built up5 . 
The earlier speciﬁcation languages, which are studied and/or used in practice even now, are 
5The concrete language is TLA+, but the paper illustrate some general problems and solution. 
4.3. LOGIC BASED SOFTWARE TECHNOLOGIES 
•	VDM (Vienna Deﬁnition Method), whose development started in the late seventies, the ﬁrst detailed report is [17], and 
•	Z, which was developed through the 1980s, the ﬁrst reference manual was published in 1989: [78]. 

[51] and [50] are thorough tutorials of VDM and Z respectively. 
Stepwise reﬁnement is the focus of these tools. The speciﬁcation language helps the speciﬁcation of the data types used in the system and the speciﬁcation of states and state transformations (that is speciﬁcation of programs). The speciﬁcation consists of two parts, the ﬁrst is the deﬁnition of non logical symbols this is done by set theoretical formalism. In the case of the deﬁnition of data types the second part consists of axioms, in the case of deﬁnition of program modules consists of their speciﬁcations (usually in the form of preand postconditions). 
The steps of program development consist of deﬁning reﬁnements of the existing deﬁnitions and proving the correctness of the reﬁnements. The reﬁnements may create new speciﬁcations in the same logics in this case the correctness proof can be supported by one of the calculi for the logic used in the system (generally the ﬁrst order one). However in several case the reﬁnement interprets a data type of the higher level speciﬁcation in another data type (e.g. sets are interpreted in sequences). In this then transformation between logics has to be handled. At the end of the reﬁnement process the speciﬁcations are transformed into programs for this purpose special calculus is provided, similarly to the FloydHoare calculus. 
There are several studies comparing the two systems, like [16], [47]. They mostly conclude that there are neither important theoretical nor practical differences between the two systems. Naturally the two systems diﬀer in several points of view, we think that the main diﬀerence is that relational algebraic operators including operators for the speciﬁcation of relational data bases are built into Z. Both systems uses naive set theory for speciﬁcation, however 
[38] argues that the theory of hereditary ﬁnite sets would be adequate for this purpose. 
The most recent system following the same line is the B method, which is able to handle object oriented systems too at least in some extent. To learn more about is visit www.bcore.com. 
There are systems which combines speciﬁcation with veriﬁcation: a speciﬁcation of a complex system can be described by them, and there a proof procedure is provided to prove correctness: 
•	ESC/Java is a programming tool for ﬁnding errors in Java programs at compile time, which uses program veriﬁcation techniques. See research.compaq.com/SRC/esc. 
•	TLA+, which is the extension of time logic with actions. [58] is a detailed introduction to the speciﬁcation language, and it illustrates in de

tails how to use such a speciﬁcation language. For more information visit http://research.microsoft.com/users/lamport/tla/tla.html. 
•	Spin is a popular software tool that can be used for the formal veriﬁcation of distributed software systems. The tool was developed at Bell Labs in the original Unix group of the Computing Sciences Research Center, starting in 1980. [49] presents techniques of using the SPIN model checker to verify correctness requirements for systems of concurrently executing processes. For more information visit spinroot.com/spin/whatispin.html. 
•	PVS is a veriﬁcation system: that is, a speciﬁcation language integrated with support tools and a theorem prover. The interested reader may visit pvs.csl.sri.com. 
•	HOLZ is a proof environment for Z and HOL6 speciﬁcations on the one hand and the generic theorem prover Isabelle on the other, see abacus.informatik.unifreiburg.de/holz. 

The systems outlined show that program veriﬁcation is in the main stream of computer science, and it is suitable for practical applications. However, proving the correctness of systems demands huge resources, both in the computing and in human resources to create the speciﬁcation of the system and to outline the plan of the proof. However in critical safety systems program veriﬁcation is applied. [59] describes the use of TLA+ by an Intel processor design group. 
6HOL is for higher order logic. 
Chapter 5

KNOWLEDGE BASED SYSTEMS 
One of the main ﬁelds of Artiﬁcial Intelligence (AI) is automatic problem solving. In the last decades this ﬁeld has given birth to several practical results, ﬁrst expert systems, later knowledge based systems are spoken about and produced in software industry. A knowledge based system basically consists of two constituents: the knowledge base and the reasoning engine. In case of the traditional program systems the domain speciﬁc knowledge is hidden in the code; therefore it is diﬃcult to verify, and almost impossible to maintain the system. On the other hand, in the case of knowledge based systems knowledge is stored in the knowledge base in descriptive form. The content of the knowledge base is interpreted by the reasoning engine. [74] provides a thorough and practical study of logic based problem solving. 
It is a natural idea to chose a logic as knowledge representation language in this case the reasoning engine is a corresponding theorem prover produced for the selected logic. However there are diﬃcult problems, the most important ones are listed below. 
•	The combinatorial explosion may spoil the eﬀectivity of the theorem prover as a reasoning engine. Therefore sometimes speciﬁc segments of logics are considered as knowledge representation language, like logic programming languages. 
•	The amount of represented knowledge is usually quite great, the search for the relevant knowledge for a problem or query is one of the greatest problem. Therefore knowledge must be structured1 . The concept frame has been introduced for this purpose, or some kind of object oriented models is used. In these cases subordinate use of logic is typical: constraints can be expressed as formulas, methods formed in logic programming languages. 

1Notice that we have met similar situation when software speciﬁcation was discussed. 
39 
There is a recent approach in logic called labelled deduction, which introduces and studies structures of formulas as ,,data base” instead of set of formulas as theories (see [26]). 
•	In most domains of practice (like medicine, geology etc.) the strictness of logics is a barrier of its application as knowledge representation language. There are no clear cut deﬁnitions, the statements are meant ,,in general” or ,,or normally”, and tools for exception handling is missing in logic. To compensate the lack of exception handling a new branch of proof systems was developed: nonmonotonic reasoning, which is discussed in the next section. 
•	Again in most domains the characteristic reasoning of the discipline is not the deduction as formalized in mathematical logics. Therefore diﬀerent ways of plausible reasoning studied by philosophical logic are studied by researchers and are used in knowledge based systems. 

The methodical development of knowledge based systems may also use some kind of logics, e.g. logic based induction may help knowledge acquisition. In the speciﬁcation of knowledge bases now the ﬁrst step is to describe the ontology of the system. The word ontology is borrowed from philosophy, however with a modiﬁed meaning. It is used in diﬀerent senses, see [44], according to the most sensible one the ontology of a knowledge base describes the characteristic features of the knowledge base, which features are not altered in the subsequent use. First order logic is often used as the language for ontology. 
5.1 Nonmonotonic reasoning 
5.1.1 The problem 
To illustrate the need of nonmonotonic reasoning let us see the ,,paradigmatic” example that is the sentence ,,Birds ﬂy.”, which is translated to logic with the use of bounded universal quantiﬁer as ∀x(bird(x) → f ly(x)). However what happens if the discourse is about an ostrich? To overcome the problem inference rule ∀xα(x) � α(x/t) is substituted by inference rules that does not allow substitution without constraints2 . 
Let us survey some approaches. 
The ﬁrst one was Reiter’s default logic (deﬁned in [77]), the new rules can be worded as ��α, β� β� with the meaning ,,if α is proved and β is consistent with the set of sentences generated so far, conclude that β is true”. 
Another approach is circumscription (deﬁned in [64]), which collects exceptions (maybe of diﬀerent types) and an inference step can be executed only if exceptional situation does not stand. If we go back to the paradigmatic example, the sentence about birds may be formed as ∀x(bird(x) ∧ ¬abnormalb(x) → 
2The second cartoon in www.cse.buﬀalo.edu/rappaport/663/FO3/nonmono.html illustrates the problem in a crooked way. 

5.1. NONMONOTONIC REASONING 
f ly(x)), and sentences like ∀x(ostrich(x) → abnormalb(x)) have to be added. The extensions of the diﬀerent abnormal predicates must be the minimal deﬁned relations notice the similarity with logic programming. It is not suitable to use equivalence in the deﬁnition of abnormality, since the content of the knowledge base generally is not closed, later new exceptions has to be added. If equivalence is used, it would mean the modiﬁcation of a sentence, however using the implicative form, only a new sentence has to be added. 
The above outlined approaches are basically ad hoc inference rules, and their practical use is doubtful: sometimes search strategy may eﬀect what sentences are inferred. 
However the introduced rules spoil the monotonicity of provability relation. If we go back to the paradigmatic example, let us suppose that Koko is a bird (bird(Koko)). If nothing else is known about this bird, we can conclude that Koko ﬂies (f ly(Koko)). If later we learn that Koko is an ostrich (so abnormalb(Koko) is true), the inference turns to be false the derived sentence (and all of its consequences) have to be deleted. Notice that nonmonotonicity not only hurts the purity of proof systems as deﬁned so far, but the revision of the knowledge base causes practical problems too. 
The problem of nonmonotonic reasoning has been a challenge for logicians too and new logics are worked out, like autoepistemic logic, outlined below. Moreover several logics rooted in diﬀerent motivations can be considered nonmonotonic ones, like probability logic (see [22]) or the logic of conditionals (see 
e.g. [69]). The interested reader can ﬁnd several books, papers and web places about non monotonic logics, we suggest [13], [30], and www.cse.buﬀalo.edu/˜rappaport/663/FO3/nonmono.html. 
Before discussing some questions in a more detailed way, let us speak about the root of the problem. The basic fallacy is that sentences as ,,Birds ﬂy” are not variants of universal sentences like ,,Every bird ﬂies”. Linguists call sentences like ,,Birds ﬂy” generic sentences. Such sentences state a characteristic feature of a gens, a species, a group. Sentence ,,Birds ﬂy” means that the ability of ﬂying is a characteristic feature of birds, but it cannot be concretized for every bird. It can be red as ,,Normally birds ﬂy”, and such a reading is the usual in the context of nonmonotonic logics. 
5.1.2 Autoepistemic logic 
Autoepistemic logic is connected with beliefs and changes of beliefs. It is a nonmonotonic logic that is the set of beliefs that are justiﬁed on the basis of given premises does not necessarily increase monotonically as the set of premises increases. 
Databases based on autoepistemic logic have the ability to record whether their knowledge about a ﬁxed object is complete or not. In Artiﬁcial Intelligence autoepistemic logic is intended to model the reasoning of an ideally rational agent. Let us see a simple example. 
Let us assume that one of the basic principle of the agent’s thinking is ,,If I do not believe something, it does not holds”. So far she has not learnt that ,,My ﬁrst teacher , Mr. U died ”, Since she has no basis to think so, she does not believe it. Therefore she thinks that ,,Mr... U lives”. Later she learns that ,,Mr. U died ”. Then she has to update her knowledge and beliefs about the world: 
1. ,,Mr. U lives,, and all of its consequences has to be omitted. 
2. ,,Mr. U died ” has to be added. 

3. ,,I believe that Mr. U died,, has to be added. 
4. The new set of knowledge and beliefs has to be closed under logical consequence. 
Now, we sketch some basic concepts of autoepistemic logic. Our approach for autoepistemic logic ids originated from the viewpoint of proof theory. 
The language of this logic is like an ordinary modal (propositional) logic with the diﬀerence that the operator ♦ is missing and � is denoted by B . Deﬁnition of formulas is the same as in modal logic. 
The meaning of the unary operator B is ,,believed”, so the meaning of the formula B(P) is ,,P is believed,,, where P is a propositional symbol. 
A central concept is the concept of theory (or stable theory). 
Deﬁnition 35 (stable theory)
A set T of formulas is said to be a stable theory in L if the following three
conditions hold

(i) if P1,...Pn ∈ T and P1,...Pn � Q then Q ∈ T (where � means ordinary logical consequence) 
(ii) if P ∈ T then B(P) ∈ T 
(iii) if P /
∈ T then ¬B(P) ∈ T. 
The concept of stable theory corresponds to theory in ordinary logic. Condition (iii) is remarkable. It is an inference rule of nonstandard form: if P is not a theorem then Q is a theorem where Q = ¬B(P) (a usual rule of inference is of the form: if P is a theorem then Q is also a theorem). 
An autoepistemic theory represents the information we have and our belief in a given stage (moment). It is maximal in the sense that no further conclusions could be drawn in this stage. 
If we have new information, to extend the actual stable theory has no sense. In this case another stable theory is needed. Theories can change essentially stage by stage, certain formulas are removed and others are included. As in classical logic, diﬀerent axioms (premises) can generate diﬀerent theories, the same conclusion could be true in the one theory and false in another theory. 
The following theorem concerns a stable theory generated by a set Σ of premises. 

5.1. NONMONOTONIC REASONING 
Theorem 36 (stable extension)
An autoepistemic theory T is a stable extension of the formula set Σ if it is the
least set of sentences satisfying the following conditions:

(i) Σ ⊆ T , 
(ii) T is closed under ordinary logical consequence (� relation of classical logic), 

(iii) if P ∈ T then B(P ) ∈ T , 
(iv) if P /
∈ T then ¬B(T ) ∈ T. 
Clearly the stable extension of Σ is the minimal stable theory containing Σ. 
The concepts of stableness can be characterized using semantics, too. It can be proven that the bit modiﬁed semantics of the modal logic S5 can be considered as a possible semantics of autoepistemic logic. 
About autoepistemic logic see e.g. [65], [31]. 
5.1.3 Nonmonotonic consequence relations 
While in the study of nonmonotonic logics ﬁrst diﬀerent calculi were suggested, to focus the study of nonmonotonic logics on their consequence relation was ﬁrst proposed by [25]. His proposal was followed by D. Lehman and his coworkers, they created a theory of nonmonotic consequence relation comprising both proof and model theoretical aspects (see e.g. [55]). 
Let us introduce a symbol �n as a binary relation between formulas, and let us call expressions like α �n β conditional assertions, with the following intuitive meaning: ,,if α holds, then normally β holds”. Notice that in a conditional assertion α has to be true according to the semantics of classical logic, and the word ,,normally” is applied only to β. Using our example: ,,Birds ﬂy” can be written as bird(x) �n fly(x), or b �n f in propositional form. The introduced symbol �n is a metapredicate, does not belong to the alphabet of the object language. However we stipulate that conditional assertions occur in the knowledge base. A nonmonotonic inference rule infer conditional assertion from conditional assertions. Notice also that this interpretation of nonmonotonic reasoning is in accordance with the interpretation of generic sentences in natural languages. Moreover, some kind of concept of ,,normal world” can be deﬁned: 
a model A is normal w.r.t. α if and only if for every β which is the consequence of α (α �n β), A � β holds. 
[25] proposed to accept three characteristic features of nonmonotonic consequence relation (compare them with the properties of provability relation): 
α �n α Reﬂexivity
α ∧ β �n γα �n β

Cut 
γ
α �n
α �n βα �n γ

Cautious Monotonicity 
γ
α ∧ β �n 
The above presented features characterize the nonmonotonic consequence relation independently of the logical connectives of the logic that is why the rule of the substitution of equivalent formulas is missing. [55] completes the characteristics of nonmonotonic consequence relation with the following two rules: 
→ βγ �n α
� α 
Right Weakening 
β
γ �n 
↔ βα �n γ
� α 
Left Logical Equivalence 
γ
β �n 
→α, α�γ 
Notice that Left Logical Equivalence is weaker than Left Weakening holding at traditional provability relation: �ββ�γ . Changing Left Weakening is important in nonmonotonic consequence relation, as it can be illustrated by our paradigmatic example. 
Let us assume that we have the following axioms: ∀x(ostrich(x) → bird(x)), ∀x(mad´
ar(x) ↔ bird(x)) and conditional assertion bird(x) �n f ly(x) is in the knowledge base. It can be inferred by Left Logical Equivalence that mad´
ar(x) �n f ly(x), however ostrich(x) �n f ly(x) can not. 
Deﬁnition 37 (cumulative consequence relation)
A consequence relation is said to be cumulative if and only if it contains all
instances of Reﬂexivity axiom and is closed under the inference rules Cut, Cau
tious Monotonicity, Right Weakening and Left Logical Equivalence.

Cumulative consequence relations can be characterized by semantic means too, namely by a generalization of Shoham [1984]. The intuitive idea is that there is a ,,more preferred” relation on the class of models, and a conditional assertion α �n β holds if and only if β holds the most preferred models of α. 
[55] generalizes this idea. The concept of state is introduced, which is a set of models, and the ,,more preferred” relation are deﬁned between states. 
Deﬁnition 38 (cumulative model) 
A triple �S, l, �� is a cumulative model if and only if 
(i) S is a set called the set of states, 
(ii) l is a function labeling every state with a non empty set of models, 

(iii) � is a binary relation on S satisfying the smoothness condition deﬁned below. 
For the next deﬁnition the notion minimal is generalized for arbitrary binary relation �: s (s ∈ A) is minimal w.r.t. � if and only if there is no z ∈ A such that z � s. 
Deﬁnition 39 (smoothness) 
Let A be a set, and let � be a binary relation on A. It is said that B ⊆ A is smooth w.r.t. �, if and only if for every element t ∈ B if t is not minimal w.r.t. �, then there is an element s of B such that s is minimal w.r.t. �. 
A state s satisﬁes a formula α if and only if every model in l(s) satisﬁes α. In the following deﬁnitions �
α denotes the set of states satisfying α. 

5.2. PLAUSIBLE INFERENCE 45 
Deﬁnition 40 (smoothness condition) 
A relation � in a cumulative model �S, l, �� satisﬁes the smoothness condition if and only if for every formula α the set �
α is smooth w.r.t. �. 
Deﬁnition 41 (cumulative consequence relation) 
Let a cumulative model W = �S, l, �� is given. The consequence relation generated by W (denoted by �W ) is as follows: 
n 
α �W β if and only if for any s minimal in �αs satisﬁes β. 
n 
Theorem 42 (representation) 
A consequence relation is a cumulative consequence relation if and only if it is generated by some cumulative model. 
The concept of cumulative consequence relation can be reﬁned adding new plausible rules; similarly the concept of cumulative model can be modiﬁed by restricting the function l and/or relation �. 
It is interesting that for any proposed nonmonotonic calculus there can be found some plausible property of the consequence relation which is not satisﬁed. 
[55] quotes some properties which are not satisﬁed even their proposed system. These are diﬀerent from the inference rules presented so far, namely they regard the absence of certain pairs from the consequence relation. Let us see an example: 
α �n γβ �n γ 
α ∨ β �n γ Disjunctive Rationality 
We may conclude that the research of the consequence relation provides a deeper insight in nonmonotonic logics, however we do not have yet a system which would satisfy all the plausible demands on nonmonotonic reasoning. 

5.2 Plausible inference 
Logic was developed with the purpose to characterize sound human reasoning in general. However in the 20. century research in logics provides the formalization of special reasoning characteristic of diﬀerent disciplines, domains. Moreover, the formal reasonings turn to be practical tools in knowledge based systems. Therefore several ways of plausible reasoning got into the focus of research, namely induction, abduction, retroduction, diﬀerent similarity based reasoning (analogical reasoning, case based reasoning). It is hard to clarify even the concept of plausible reasoning. Strictly speaking every non sound reasoning belongs to it. Plausible reasoning is sometimes characterized that the result of some plausible proof can be defeated (refuted). If this property is in focus, the term defeasible reasoning is used [75]. In D. M. Gabbay’s opinion the main characteristic of plausible reasoning is that diﬀerent chains of inference for and against a statement have to be weighted to reach a decision. 
In another approach plausible reasoning is rather taking hypotheses than inferring a statement. So the scheme of plausible reasoning is as follows: 
1. generating hypotheses, 
2. accepting the most plausible one if human intuition does not help, some kind of search strategy can do it, 
3. testing the accepted one this can be done by deduction. 

For the ﬁrst step, for hypotheses generation special logical calculi may be introduced. We only discuss induction and retroduction in short. 
Induction is a well known term of philosophical logic, it means to extract general rule from examples. In AI induction can be used in several ﬁelds such as learning, knowledge extraction. 
The term retroduction as a way of reasoning, was ﬁrst used by the outstanding American mathematician, Pierce. It is a backward reasoning like reasoning in diagnostic problems (in medicine as well as in technical problems) and crime detection. 
Both induction and retroduction can be considered the inverse of deduction: the inference rules have to be reversed. Such a calculus keeps falsity instead of truth. To show an example of an non deductive inference rule, and to illustrate the diﬀerence between the ways of reasoning, let us see the case of Modus Ponens: 
α → β, α � β deduction 
α, β �ind αβ induction: 
→	if in the cases when α holds, β also holds, then αβ can be assumed as a hypothesis → 
α → β, β �ret α retroduction: 
knowing the rule αβ and having β, α can be assumed as a 
hypothesis → 
Note that the above rules for induction and retroduction outlines only the logical nature of the plausible inference in question: the inference rules to be applied in knowledge based systems include a lot of conditions which can be considered as elements of plausible search strategies. 
Knowledge representation is a very widespread topic: there is several methods, whose connection with logic may be quite diﬀerent. Here we have shown some logical problem, which was raised by this subjects. The most important topic we have omitted is how to represent uncertain information. Beside probabilistic logic (see [22]) fuzzy logic is an important tool for this purpose, the interested reader may start with www.aaai.org/AITopics/html/fuzzy.html. 

5.3 Great projects in reasonings 
Reasoning has been and will be one of the great challenges to computing. There were several somewhat naive beliefs in the sixties that some universal problem solving techniques, theorem provers for classical logic may provide solution. 
Below we give some of the recent great projects trying to create automatic system that can reason: 
5.3. GREAT PROJECTS IN REASONINGS 
•	ACTR is a cognitive architecture: a theory about how human cognition works. The system has a modular structure with diﬀerent modules being directly related to particular areas in the brain, their activation in various tasks being conform to functional brain imaging data ([8]). ACTR claims that cognition emerges out of the interaction between speciﬁc units of procedural and declarative knowledge. For information visit http://actr.psy.cmu.edu/about/ 
•	JTP is an artiﬁcial reasoning system developed on the foundation of Prolog. The JTP architecture, at the top level of abstraction, is independent of the representation language; the implemented system uses a ﬁrst order logic representation language, called KIF [54]. JTP is a hybrid system in the sense that it combines general purpose reasoners with special purpose ones, the latter embodying both domain speciﬁc and task speciﬁc expertise. 
•	Soar has its roots in classical theories of AI. According to Soar a cognitive architecture is a theory of ﬁxed mechanisms and structures that underlie human cognition. The behavior (as the product of the architecture and the content) takes place in a problem space. It unfolds from an initial state to reach the (or one of the) state(s) where the goal is achieved. The resolution of an impasse also leads to learning. There is an extension of Soar for abduction (AbdSoar), which uses operators: cover; resolveredundancy, resolveinconsistency, determinecertainty, determineaccountsfor, markredundancies, and markinconsistencies. The interested reader may start with [61]. 

Chapter 6

Logic and Complexity theory 
There is a close traditional connection between Logic and Algorithm theory, Logic and Automaton theory and between Logic and Complexity theory (e.g. there are elegant proofs for Incompleteness theorems, undecidability of ﬁrst order logic using the concept of Turing machine). Here we sketch some results mainly on the connections of Logic and Complexity theory. 
We suppose a minimal knowledge on basic concepts of computability and complexity theory: the concepts of the most known complexity classes P and NP, that of completeness with respect to a given complexity class, the reducibility of a problem to another one, etc.. We accept here the hypothesis P =�NP, as usual. 
There are classical results in Complexity theory which are related to Logic. These are connected with important logical problems which are complete with respect to a given complexity class. Such a logical problem is the problem SAT that is the problem of satisﬁability of a propositional formula given in conjunctive normal form. As it is known, SAT is a NPcomplete problem. As regards the concepts and results above see [72] in this Volume. A similar problem is the problem HORNSAT, that is the problem of satisﬁability of a ﬁnite set of propositional Horn clauses. It is known that HORNSAT is a Pcomplete problem. Other similar problems originated from logic are: the problems 3SAT, Max2SAT, etc.. 
Problems above as complete problems are characteristics of a given complexity class. These kinds of results are important also from the viewpoint of applications. For example the fact that HORNSAT is in P is a base of logic programming (PROLOG is based on SLD algorithm concerning problem HORNSAT). 
There is a less traditional connection between Logic and Complexity theory which is more direct and comprehensive. This connection is a bit similar to the logicalgebra connection. This is a kind of translation from complexity theory to 
49 
logic and viceverse. More exactly: given a complexity class C we try to ﬁnd a logical language S and a set Σ of formulas in S such that with every problem Q (or with a problem equivalent to Q) in C, we can associate a formula in Σ which formalizes Q. And conversely with any formula in Σ one can associate a problem in C. 
The language of ﬁrst order logic is not suitable for choice of S, some extensions are needed. The main reason is that the concept of recursion is not expressible in terms of a ﬁrstorder language. The usage of secondorder logic and its language seems to be suﬃcient. This is conﬁrmed by the following theorem: A language S is ,,recognized” by an automaton if and only if S is ,,deﬁnable” in (monadic) second order logic. 
The language S chosen for the characterization of complexity classes is the second order language of graphs. The class of models is restricted to the class of ﬁnite graphs. S contains only the binary relation symbol E, interpreted as ,,to be an edge” of the graph. Only relation variables (and no function variables) are used: one nary relation variable Pn for every natural number n. 
The class of formulas of the form ∃Piψ(Pi,x1,...xk) is considered, where Pi is the only relation variable, and x1,...xk are the free individuum variables in ψ. 
Deﬁnition 43 (∃Pψ graph problem)
,,The ∃Pψ graph problem”: Is the formula ∃Piψ(Pi,x1,...xk ) true for a given

ﬁnite graph G = G,EG and evaluation �a1,...ak �∈Gk ? 
For example let us see the property ,,unreachability” in graphs that is the property ,,there is no path between given two nodes”. A possible formalization of this property is 
∃P(ρ∧¬P(x,y)) 
where ρ = u∀v∀w(Puu ∧(Euv → Puv) ∧(( Puv ∧Pvw) → Puw)). Here P
∀
should be a reﬂexive, transitive relation containing E. The formula says that there is such a reﬂexive, transitive closure of E for which P(x,y) is not satisﬁed. 
Theorem 44 (Fagin)
Any ∃Pψ graph problem is in NP and conversely, every decision problem of
graphs which is in NP can be reduced to a ∃Pψ graph problem.

The next question is: how to characterize the problems in P inside NP, using logic. 
Recall that a prenex normal form is a strong Skolem form if its preﬁx contains only universal quantiﬁers (it is an universal formula) and the kernel is of conjunctive normal form. A Skolem form is a Horn formula if in any conjunction of the kernel there is at most one literal without negation. 
Deﬁnition 45 (second order Horn formula) A formula ∃Pψ ∈Σ is a second order Horn formula if ψ is a Horn formula with respect to P (the members of the conjunctions in the kernel of ψ are allowed to contain P at most once without negation). 
For example the conjunction members P uu, ¬Euv∨ P uv, ¬P uv ∨¬P vw ∨P uw, ¬P xy of the Skolem form of formula ∃P (ρ ∧¬P (x, y)) satisfy this condition, therefore this Skolem form is a secondorder Horn formula. 
It is not diﬃcult to check that if ∃P ψ is a second order Horn formula then the ∃P ψ graph problem is in P (for example the problem ,,unreachibility”). Unfortunately the converse of this proposition fails to be true, a modiﬁcation is needed. 
Let us consider linear ordered graphs rather than ,,ordinary” graphs. The ordering is deﬁned for the vertices of the graph. Linearity means that the ordering is irreﬂexive, trichotome and transitive. Let us extend the language S by a binary relation symbol R which is always interpreted as a linear ordering. 
We can deﬁne a new problem called ∃P ψ ordered graph problem similarly to the ∃P ψ graph problem but restricting the graphs (the models) in the original deﬁnition to linear ordered graphs. 
Intuitively, with an ordering of a graph we can associate a sequence of the elements of the graph. These elements, in the given order can serve as input for an automaton (e.g. a Turing machine). 
The following theorem gives a logical characterization for the class P: 
Theorem 46 (characterizing class P ) 
(i) If ∃P ψ is a Horn formula of second order then the ∃P ψ problem is in 
P. 
(ii) Every decision problem of ordered graphs in P can be reduced to a ∃P ψordered graph problem. 

Many other complexity classes can be characterized using logic. In order to do this diﬀerent kinds of logics are needed. The so called ,,ﬁxedpoint logics” seem to be very adequate tool for this purpose. Complexity classes P, PSPACE, LOGSPACE, NLOGSPACE can be characterized as the ﬁnitely axiomatizable classes in certain ﬁxedpoint logics. 
We conclude this point by some remarks concerning applications and advantages of the connection between logic and complexity theory. 
•	This connection may help to recognize that a concrete problem is in a given complexity class (by expressing the problem in a suitable logical language), and it may allow us a better understanding of a given complexity class using the given logic. 
•	Logical characterizations allow us to convert problems, methods and results of complexity theory into logic and vice versa (for example, the statements LOGSPACE=SPACE �or P=NP can be converted to logical statements and they can be investigated in logic, too). 
•	This connection allow us to consider a logical language associated with a given complexity class also as a programming language of higher level. 

And conversely, given a programming language, considering it as a logical language we can try to ﬁnd a complexity class associated with this language. These kind of connections are intensively investigated for diﬀerent programming languages, among others for some kinds of the language DATALOG. 
References to this section are e.g.: [20], [71], [72], [14], [82], [83]. 

Bibliography

[1] S. Abramsky, D.M. Gabbay, T.S.E. Mainbaum (ed), Handbook of Logic in Computer Science I., Background, Mathematical Structures, Oxford University Press, 1992 
[2] S. Abramsky, D.M.	Gabbay, T.S.E. Mainbaum (ed), Handbook of Logic in Computer Science II., Background, Computational Structures, Oxford University Press, 1992 
[3] S. Abramsky, D.M. Gabbay, T.S.E. Mainbaum (ed), Handbook of Logic in Computer Science III., Semantic Structures, Oxford University Press, 1992 
[4] S. Abramsky, D.M. Gabbay, T.S.E. Mainbaum (ed), Handbook of Logic in Computer Science IV., Semantic Modelling, Oxford University Press, 1992 
[5] S. Abramsky, D.M. Gabbay, T.S.E. Mainbaum (ed), Handbook of Logic in Computer Science V., Theoretical Methods in Speciﬁcation and Veriﬁcation, Oxford University Press, 1992 
[6] S. Abramsky, D.M.	Gabbay, T.S.E. Mainbaum (ed), Handbook of Logic in Computer Science VI., Logical Methods in Computer Science, Oxford University Press, 1992 
[7] Acz´el P., An introduction to inductive deﬁnitionsin, J. Barwise (ed.) Handbook of Mathematical Logic NorthHolland, 1977 pp.739781 
[8] Anderson J., D. Bothell, M. Byrne, C Lebiere, An Integrated Theory of the Mind, 2002 
[9] Andr´eka H., N´emeti I., Completeness of Floyd Logic, in Bull. Section of Logic, 7, Wroclav, 1978 pp. 115120 
[10] Andr´eka H., N´
emeti I., Sain I., On the strength of temporal proofs, Theoretical Computer Science 87 1991 
[11] Antonelli,	A., Nonmonotonic Logic, The Stanford Encyclopedia of Philosophy (Summer 2003 Edition), Edward N. Zalta (ed.), URL = <http,//plato.stanford.edu/archives/sum2003/entries/logicnonmonotonic/> 
53 
[12] Apt K, Bol R, Logic Programming and Negation, a Survey Journal of Logic Programming, 1920, 1994, pp.,971 
[13]	Artiﬁcial Intelligence, Volume 157, issues 12, 2004 
[14] Ben, A. M., Amram, N.D., Computational complexity via programming languages, constant factors do matter, Acta Informatica, 37, 2, 2000 
[15] Bibel, W., Schnitt, P.H., Automated Deduction. A Basis for Applications, I., Kluwer, 1991 
[16] Bjørner D., Hoare C.A.R., Langmaack H., VDM and Z	Formal Methods, in, Software Development, Lecture Notes in Computer Science, 428, Springer Verlag, 1990 
[17] Bjørner D., Jones C.B. (ed), The Vienna Development Method, the MetaLanguage, Lecture Notes in Computer Science 61, Springer Verlag, 1978 
[18] Caﬀera, R., Salzer, G.(Ed.), Automated Deduction in Classical and Nonclassical Logics, Lecture Notes in Comp. Sci., 1761, Springer, 2000 
[19] Denecker, M., Kakas, A.C., Abductive logic programming, J. of Logic Programming, 44, 12, 2000 
[20] Ebbinghaus, H., Flum, J., Finite Model Theory, Springer, 1999 
[21] Ferenczi, M., Mathematical Logic, Muszaki Kiado, (in Hungarian), 2001 
[22] Ferenczi, M., Classical and nonclassical logics, in this Volume 
[23] Fitting,M. A KripkeKleene semantics for logic programming, The Journal of Logic Programming, 4, 1985, 295312 
[24] Floyd R.M., Assigning meaning to programs, in J.T. Schwartz (ed.) Proc. Symp. in Applied Mathematics, AMS, Providence, RI, 1967 pp.1932 
[25] Gabbay D.M., Theoretical foundations for nonmonotonic reasoning in expert systems, in K.R. Apt (ed) Proceedings of NATO Advanced Study Institute on Logics and Models of Concurrent Systems Springer, Berlin 1985, pp. 439457 
[26]	Gabbay D.M., Labelled Deductive Systems, Oxford Logic Guides 33.Calderon Press, Oxford 1996 
[27] Gabbay D.M., Guenther F. (ed), Handbook of Philosophical Logic, 2. ed. Volume 19, Kluwer Academic Publisher, 2001, 2002 
[28] Gabbay D.M., Hogger C., Robinson J.	(ed), Handbook of Logic in Artiﬁcial Intelligence and Logic Programming I, Logical foundations, Oxford University Press, 1993 
BIBLIOGRAPHY 
[29] Gabbay D.M., Hogger C., Robinson J. (ed), Handbook of Logic in Artiﬁcial Intelligence and Logic Programming II, Deduction methodologies Oxford University Press, 1993 
[30] Gabbay D.M., Hogger C., Robinson J. (ed), Handbook of Logic in Artiﬁcial Intelligence and Logic Programming III, Nonmonotonic Reasoning and Uncertain Reasoning, Oxford University Press, 1994 
[31] Gabbay D.M., Hogger C., Robinson J. (ed), Handbook of Logic in Artiﬁcial Intelligence and Logic Programming IV, Epistemic and Temporal Reasoning, Oxford University Press, 1995 
[32] Gabbay D.M., Hogger C., Robinson J.	(ed), Handbook of Logic in Artiﬁcial Intelligence and Logic Programming V, Logic Programming Oxford University Press, 1996 
[33] Gentzen,G., Untensuchungen ¨
uber das logische Schliessen, Meth.Zeitschrift 39, 1934 
[34] Gergely T., Sz˝ots M., On the incompleteness of proving patial correctness, in Acta Cybernetica 4 1978 pp. 4557 
[35] Gergely, T., Szab´
o, Zs., Fixedpoint equations as hypothesis in inductive reasoning, Proc. on Artiﬁcial Intelligence and Inductive Inference, LNCS, Springer, 1987 
´ 
[36] Gergely T, Ury L., Program behaviour speciﬁcation through explicit time consideration, in S.H. Lavington (ed), Information Processing ‘80, North Holland 1980 
´ 
[37] Gergely T.,	Ury L., FirstOrder Programming Theories EATCS Monographs on Theoretical Computer Science 24, Springer Verlag 1991 
´ 
[38] Gergely T, Ury L, A unique logical framework for software developmentin, Artiﬁcial Intelligence News Intelligent System Laboratorium, Moscow, pp. 6281 1993 
[39] Girard, J. Y.,	Proof theory and logical complexity I., Bibliopolis Naples, 1987 
[40] Girard, J.Y., Linear Logic, in Theoretical Computer Science 50 pp.1102 
[41] Goerdt, A., DavisPutnam resolution versus unrestricted reolution, in Logic and Combinatorics, Baltzer, 1992 
[42] Groenendijk, Stokhof, Dynamic Predicate Logic. Towards a compositional and nonrepresentational discourse theoryms, Amsterdam, ITLI 1987 
[43] Gu, J., Franco, j., Purdom, P.W., Wah, B.W., Algoritms for the Satisﬁability Problem, Cambridge Univ. Press, 2001 
[44] Guarino N., Giaretta P., Ontologies and Knowledge Bases, Towards a terminological Clariﬁcation, in N.J.I. Mars (ed.) Toward a Very Large Knowledge Bases IOS Press, Amsterdam, 1995 
[45] Harel, D., D. Kozen, J.Tiuryn, Dynamic Logic, in [27], Volume 4. 
[46] Harel, D., Tiuryn, J., Dynamic Logic, MIT Press, 2000 
[47] Hayes I., VDM and Z, A Comparative Case Study Formal Aspects of Computing 4, 1992 pp.7699 
[48] Hoare C.A.R., An axiomatic basis for computer programming, Communication of ACM, 12, 1969 pp.576580 
[49] Holzmann, G.J., The SPIN Model Checker , Primer and Reference Manual, Addison Wesley 2004 
[50] Jacky,	J, The Way of Z, Practical Programming with Formal Methods, Cambridge University Press 1997 
[51] Jones C.B., Systematic Software Development using VDM, Prentice Hall, New York 1994 
[52] Joshi, R., Leino K.R., A semantic approach to secure information ﬂow Science of Computer Programming 37, 2000 pp.113138 
[53] Kakas	A.C., Riguzzi,F., Abductive Concept Learning, New Generation Computing 18, 2000 pp.243294 
[54] Knowledge Systems Laboratory,	Stanford University, JTP, An ObjectOriented Modular Reasoning System, www.ksl.stanford.edu/software/JTP, July 24, 2003 
[55] Kraus S., Lehman D.,Magidor M., Nonmonotonic Reasoning, Preferential Models and Cumulative LogicsArtiﬁcial Intelligence 44, 1990 pp.167207 
[56] Kr¨oger F., Temporal Logics of Programs, Spriger Verlag, Berlin 1987 
[57] Lamport, L., ’What is good in temporal logic?	in Mason R.E.A. (ed.), Information Processing’83, North Holland, 1983, pp. 657668. 
[58] Lamport, L., Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, Pearson Education, Inc. 2002 
[59]	HighLevel Speciﬁcations, Lessons from Industry, Springer Verlag, 2003 
[60] Lamport,	L., Paulson, L. C., Should your speciﬁcation language be typed? SRC Research Report 147, Digital Systems Research Center, Palo Alto, CA, May 1997. Available at http://www.research.digital.com/SRC, http://citeseer.ist.psu.edu/article/lamport98should.html 
BIBLIOGRAPHY	57 
[61] Lehman,	J.,. J. Laird, P. Roesmbloom, A Gentle Introduction to Soar, an Architecture of Human Cognition, www.eecs.umich.edu/˜soar/docs/Gentle.pdf 
[62] V.	Marek and M. Truszczynski, Stable models and an alternative logic programming paradigm, in The Logic Programming Paradigm, a 25Year Perspective, 1999. 
[63] MartOliet,N., Meseguer,J.,	Rewriting Logic as a Logical and Semantic Frameworkin [27], Volume 7 
[64] McCharthy J., Circumscription, A form of nonmonotonic reasoning, in Artiﬁcial Intelligence 13 1980 pp.2739 
[65] Moore, R.C., Autoepistemic logic, in Nonstandard Logics for Automated reasoning, Academic Press, 1988 
[66] Muggleton S., Foundation of Inductive Logic Programming, Prentice Hall, Englewood Cliﬀs, N.Y., 1995 
[67] Muggleton S., Page D. (ed), Special Issue on Inductive Logic Programming Journal of Logic Programming 40 No2/3, 1999 
[68] Nipkow,T.,	Paulson,L.C., Wenzel,M., Isabelle/HOL A Proof Assistant for Higher Order Logic, Volume 2283 of Lecture Notes in Computer Science, Springer Verlag; 2002 http://www.4.in.tum.de/˜nipkow/LNCS2283/download.html 
[69] Nute D., Cross, Ch., Conditional Logic, in [27], Volume 4. 
[70] Paulson, L.C., Designing a Theorem Proverin [2], pp.416477 
[71] Papadimitriou, C. H., Computational Complexity, AddisonWesley, 1995 
[72] Pinter,M., Ronyai, L. Eﬃcient algorithms, in this Volume 
[73] Pnueli, A., The temporal logic of programs, in Proc. 18th IEEE Annual Symp. on Foundation of Computer Science, Providence, RI 1977 pp. 4657 
[74] Poole D., Mackworth A., Goebel R., Computational Intelligence, A Logical Approach, Oxford University Press 1998 
[75] Prakken,H., Vreeswijk,G., Logics for Defeasible Reasoning, in [27] Volume 4 
[76] Prawitz, D, Natural Deduction, Almquist & Wiksell, Upsala, 1965 
[77] Reiter R., Nonmonotonic reasoning, in Annual Reviews in Computer Science 2, Annual Reviews Inc. 1980 pp.147186 
[78] Spivey. J.M., Understanding Z, A Speciﬁcation Language and its Formal Semantics, Cambridge Tracts in Theoretical Computer Science 3 Cambridge Universitz Press, 1988 
[79] Sundholm, G., Systems of Deduction, in [27], Volume 2. 
[80] Sz˝ots M., A general paradigm of logic programming, in Beyond Number Crunching, J. von Neumann Soc., Budapest, 1986 
[81] Turini, F., Krzysztof, A.(Ed.)	Metalogics and Logic Programming, MIT Press, 1995 
[82] Urquhart, A., The relative complexity of resolution and cutfree Gentzen systems, in Logic and Combinatorics, Baltzer, 1992 
[83] Urquhart, A., The complexity of propositional proofs, J. of Symbolic Logic, 1, 1995 
[84] Van Gelder A., Ross K., Schipf J., The WellFounded Semantics for General Logic Programs, in Journal of ACM 38 1980 pp.620650 
[85] Wand, M., A new incompleteness result for Hoare System Information and Control 56, 1978 pp.7299