A concrete deskolemization algorithm

2 downloads 271 Views 925KB Size Report
Jul 8, 2014 - Bachelor thesis. Computer Science. Radboud University. A concrete deskolemization algorithm. Author: Ramon
Bachelor thesis Computer Science

Radboud University

A concrete deskolemization algorithm

Supervisor/assessor: dr. Freek Wiedijk

Author: Ramon van Sparrentak 0757276

Second assessor: prof. dr. Herman Geuvers

July 8, 2014

Abstract Skolemization is a common transformation in automated theorem provers. This paper presents an implementation of the reverse process, deskolemization of a proof in sequent calculus. The implementation is based on work of M. Baaz, S. Hetzl and D. Weller in On the complexity of proof deskolemization.

Contents 1 Introduction 1.1 Drinker paradox . . . . . . 1.2 Automated theorem provers 1.3 Skolemization . . . . . . . . 1.4 Example . . . . . . . . . . .

. . . .

2 2 2 3 3

2 Proof deskolemization 2.1 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

5 5

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

3 Definitions 7 3.1 Expansions and LKE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 Example of an expansion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4 Structural Skolemization 12 4.1 Example of Skolemization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 5 Proof deskolemization 5.1 Expansion extraction . . . . . . . . . . . . . . . . 5.2 Example of expansion extraction . . . . . . . . . 5.3 Skolemized expansion to deskolemized expansion 5.4 Example of expansion deskolemization . . . . . . 5.5 Proof in LKE from deskolemized expansion . . . 5.6 Example of proof construction in LKE . . . . . . 5.7 LKE to LK . . . . . . . . . . . . . . . . . . . . . 5.8 Example of LKE to LK . . . . . . . . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

14 14 16 17 18 18 20 20 21

6 Conclusion

23

Appendices

25

A Haskell implementation

26

1

Chapter 1

Introduction An automated theorem prover (ATP) is a computer program that tries to find a proof for a formula. Automated theorem provers are used in for example program and integrated circuit verification. These provers aid in development by proving the correctness of parts of the implementation. Finding a proof is generally not easy, and an ATP may fail to find one. A proof generated by an ATP system is unfortunately not a proof in natural deduction and is difficult to understand. Natural deduction is a proof calculus that was designed to be close to actual reasoning [4]. One of the problems in transforming a proof from clausal logic to natural deduction are the Skolem functions that are introduced by the automated theorem prover. For an user seeking a proof of a theorem an automated theorem prover gives only a proof of the Skolemized theorem. Due to the equisatisfiability of the formulas there exists a proof of the original formula. But what does the proof look like? Or how do we construct it? Obtaining a proof for a formula from proof a of the Skolemized formula is called deskolemization. This paper describes an algorithm and its implementation for deskolemizing cut-free proofs in LK. The algorithm is derived from the definitions in [7]. The remainder of this paper is organized as follows. In section 1.1 the drinker paradox is explained which is used as a running example. In section 3 the calculus is described. Section 4 explains Skolemization and finally in section 5 the deskolemization.

1.1

Drinker paradox

The drinker paradox will be used in this paper as the running example. The paradox is also called the Drinkers’ Principle [10]. The drinker paradox as a first order formula is ∃x (D(x) → ∀yD(y)) In natural language the drinker paradox can be stated as There is someone in the pub such that, if he is drinking, everyone in the pub is drinking. The statement seems to be false. How can it be that if this person is drinking, then everybody must be drinking as well? There are two important points to see why the paradox is true. There is no time involved. The paradox does not claim if someone starts drinking, then everybody will drink. To show it is true, we can pick anyone we want to be the someone. Thus given any pub, pick someone who is not drinking. (If we can’t pick someone who isn’t drinking, the paradox is true since everyone is drinking). Then the paradox is true, because he or she isn’t drinking. And if this person starts to drink? Just pick someone else who isn’t drinking.

1.2

Automated theorem provers

The best automated theorem provers can be found at the CADE ATP System Competition, CASC, an annual competition for automated theorem provers [12][9]. CASC evaluates the performance of ATP systems on problems from Thousands of Problems for Theorem Provers, TPTP [11]. The winner of the CASC-24 in 2013 in the division of formulas in first order form was Vampire 2.6. Vampire and others like Prover9 use proof by refutation in clausal logic [1]. 2

Most ATP systems use proof by refutation. They assume the theorem to be false and show the negated theorem to be unsatisfiable by deriving a contradiction. A proof by refutation for the drinker paradox will show there is someone who is drinking and not drinking if the drinker paradox is false.

1.3

Skolemization

Skolemization is commonly used in ATP systems before proving a formula. Skolemization replaces existential quantifiers in a formula by Skolem functions. The resulting formula is equisatisfiable with the original formula, but is easier to prove. The Skolemized formula preserves the satisfiability of the original formula. Which means that iff there is a model that makes the Skolemized formula true then there is a model that makes the original formula true. This is an useful property in a proof by refutation. A proof by refutation proves there is no model that satisfies the negated formula, thus the formula itself must be valid. A refutation proof of a Skolemized negated formula implies there is also no model for the negated formula, and thus the formula is valid. Herbrandization is the dual of Skolemization. It eliminates universal quantifiers. Herbrandization preserves the validity of the formula.

1.4

Example

As an example we consider the case of constructing a proof in sequent calculus of the drinker paradox using Prover9, an automated theorem prover. The drinker paradox in suitable input format is formulas(goals). (exists x (D(x) -> (all y D(y)))). end_of_list. Prover9 will negate the formula, put it in prenex normal form, Skolemize it and turn it in clausal form. The resulting Skolemized form is formulas(sos). D(x). [deny(1)]. -D(f1(x)). [deny(1)]. end_of_list. The function f1 is the Skolem function introduced. The intermediate steps are ¬ (∃x (D(x) → ∀yD(y))) ¬ (∃x∀y (D(x) → D(y))) ∀x∃y¬ (D(x) → D(y)) ∀x∃y (D(x) ∧ ¬D(y)) ∀x (D(x) ∧ ¬D(f1 (x))) {D(a)}, {¬D(f1 (a))} The actual proof constructed by Prover9 is 1 2 3 4

(exists x (D(x) -> (all y D(y)))) # label(non_clause) # label(goal). -D(f1(x)). [deny(1)]. D(x). [deny(1)]. $F. [resolve(2,a,3,a)].

[goal].

Thus the drinker paradox is true. Why it is true is not clear from this proof. We could transform this proof in to a proof in LK. In sequent calculus the proof from Prover9 corresponds to a proof of ∀xD(x) ∧ ∀y¬D(f1 (y)) ` [π] ∀xD(x) ∧ ∀y¬D(f1 (y)) ` 3

With this proof we can make a refutation proof in LK for the Skolemized drinker paradox

[φ] [π] ¬ (∃x (D(x) → D(f1 (x)))) ` ∀xD(x) ∧ ∀y¬D(f1 (y)) ∀xD(x) ∧ ∀y¬D(f1 (y)) ` Cut ¬ (∃x (D(x) → D(f1 (x)))) ` The calculus in this paper does not have a Cut rule. However, Cut rules can be eliminated from a proof [5]. CERES is a system capable of eliminating cut in first order logic [2]. The proof φ is simple as the antecedent and succedent are logically equivalent. The proof of π can be created from the proof by Prover9. This proof is still not a proof of the drinker paradox. There still is a Skolem function f1 . Thus the last step necessary step to obtain a refutation proof of the drinker paradox, from the Skolemized proof of ¬ (∃x (D(x) → D(f1 (x)))) `, requires deskolemizing the proof. A method of deskolemizing, and its implementation, is explained in the following sections.

4

Chapter 2

Proof deskolemization We now present the algorithm for deskolemization, constructing a proof for a theorem from a proof of the Skolemized theorem. The algorithm takes as input a sequent S to prove and a proof π 0 of S 0 , the Skolemized S. The output is then a proof π of S. The sequent calculus, LK, for these proofs is defined in section 3. The deskolemization of a proof consists of four steps. In the first step a compact representation of the proof, an expansion, is extracted. Secondly, this expansion is deskolemized. Thirdly, a proof of the deskolemized expansion is constructed in LKE calculus. Finally, the proof in LKE is transformed into proof in LK. Let S The sequent to proof S 0 The Skolemized sequent π 0 A proof of S 0 E Expansion sequent of S E 0 Expansion sequent of S 0 , deskolemized S φ A proof of E 0 in LKE π A proof of S in LK then the process of finding a proof π of S can be depicted as πO

LK

S

LK, Skolemized

 S 0 = sk(S)

sk

ATP

/ proof π 0

rm,rmTF

e

 E0

LKE

desk

/E

Pr

/ proof φ of S

The function sk Skolemizes a sequent. Given S and π 0 the goal is to construct a proof π of S. The expansion is extracted by e from the proof, section 5.1. This expansion is deskolemized by desk, section 5.3. The proof in LKE is reconstructed by Pr and is transformed into a proof in LK by rm and rmTF.

2.1

Example

Let S =` ∃x(P (x) → ∀yP (y)) its Skolemization is S 0 = ` ∃x P (x) → P (f0 (x)). A proof π of S 0 is

5

P (f0 (a)), P (a) ` ∃x(P (x) → P (f0 (x))), P (f0 (f0 (a))), P (f0 (a)) PR1 P (f0 (a)), P (a) ` P (f0 (a)), ∃x(P (x) → P (f0 (x))), P (f0 (f0 (a))) →R P (a) ` P (f0 (a)), ∃x(P (x) → P (f0 (x))), P (f0 (a)) → P (f0 (f0 (a))) ∃Rf (a) P (a) ` P (f0 (a)), ∃x(P (x) → P (f0 (x))) PR1 P (a) ` ∃x(P (x) → P (f0 (x))), P (f0 (a)) →R ` ∃x(P (x) → P (f0 (x))), P (a) → P (f0 (a)) ∃Ra ` ∃x(P (x) → P (f0 (x))) The goal is to construct the following proof of S P (z), P (a) ` ∃x(P (x) → ∀yP (y)), ∀yP (y)), P (z) PR1 P (z), P (a) ` P (z), ∃x(P (x) → ∀yP (y)), ∀yP (y)) →R P (a) ` P (z), ∃x(P (x) → ∀yP (y)), P (z) → ∀yP (y)) ∃Rz P (a) ` P (z), ∃x(P (x) → ∀yP (y)) PR1 P (a) ` ∃x(P (x) → ∀yP (y)), P (z) ∀Rz P (a) ` ∃x(P (x) → ∀yP (y)), ∀yP (y) →R ` ∃x(P (x) → ∀yP (y)), P (a) → ∀yP (y) ∃Ra ` ∃x(P (x) → ∀yP (y))

6

Chapter 3

Definitions In this section the first order sequent calculus used in this thesis is described. It is slightly different from the calculus used in [7], > and ⊥ are omitted. Definition 1. Symbols • Variables x, y, . . . and x0 , y0 , x1 , y1 , . . . • Logical connectives ¬, ∧, ∨, → • Predicates P0 , P1 , . . . • Functions f0 , f1 , . . . • Quantifiers ∃, ∀ Definition 2. Terms • A variable symbol • An expression f (t1 , . . . , tn ) where f is a function with arity n and ti are terms Definition 3. Formulas • P (t1 , . . . , tn ) where P is a predicate with arity n and ti are terms • ¬A where A is a formula • (A1 ∨ A2 ) where A1 and A2 are formulas • (A1 ∧ A2 ) where A1 and A2 are formulas • (A1 → A2 ) where A1 and A2 are formulas • (∃xA) where x is a variable and A a formula • (∀xA) where x is a variable and A a formula The result of a substitution A [x := t] is A with all free occurrences of x substituted by t. Definition 4. Every subformula of a formula is in positive or negative context. The formula itself is in positive context. For every (sub)formula A • If A = ¬A1 is in positive context, then A1 is in negative context • If A = ¬A1 is in negative context, then A1 is in positive context • If A = A1 → A2 is in positive context, then A1 is in negative context and A2 is in positive context

7

• If A = A1 → A2 is in negative context, then A1 is in positive context and A2 is in negative context • If A = A1 ∨ A2 , A = A1 ∧ A2 , A = ∃xA1 or A = ∀xA1 then A1 and A2 have the same context parity as A A quantifier ∀x is called strong (weak) if it occurs in a positive (negative) context, a quantifier ∃x is called weak (strong) if it occurs in a positive (negative) context [7, Preliminaries]. The number of strong quantifiers in a formula A will be denoted as qocc(A). Definition 5. A sequent S = A1 , . . . , An ` B1 , . . . , Bm where A1 , . . . , An and B1 , . . . , Bm are sequences of formulas. The formulas A1 , . . . , An are in negative context and B1 , . . . , Bm are in positive context. This differs from [7] where sequents are multisets of formulas. Definition 6. Inference rules. A denote a single formula and Γ, ∆ sequences of formulas

A, Γ ` ∆, A

I

Γ ` ∆, A ¬L ¬A, Γ ` ∆

A, Γ ` ∆ ¬R Γ ` ∆, ¬A

A1 , Γ ` ∆ A2 , Γ ` ∆ ∨L A1 ∨ A2 , Γ ` ∆

Γ ` ∆, A1 , A2 ∨R Γ ` ∆, A1 ∨ A2

A1 , A2 , Γ ` ∆ ∧L A1 ∧ A2 , Γ ` ∆

Γ ` ∆, A1 Γ ` ∆, A2 ∧R Γ ` ∆, A1 ∧ A2

Γ ` ∆, A1 A2 , Γ ` ∆ →L A1 → A2 , Γ ` ∆

A1 , Γ ` ∆, A2 →R Γ ` ∆, A1 → A2

A [x := y] , Γ ` ∆ ∃Ly ∃xA, Γ ` ∆

Γ ` ∆, ∃xA, A [x := t] ∃Rt Γ ` ∆, ∃xA

A [x := t] , ∀xA, Γ ` ∆ ∀Lt ∀xA, Γ ` ∆

Γ ` ∆, A [x := y] ∀Ry Γ ` ∆, ∀xA

Ai , A1 , . . . , Ai−1 , Ai+1 , . . . , An ` ∆ PLi A1 , . . . , A n ` ∆

Γ ` A1 , . . . , Ai−1 , Ai+1 , . . . , An , Ai PRi Γ ` A1 , . . . , A n

y does not occur in A, Γ nor ∆. Definition 7. A proof π in LK of a sequent S is a tree built from inference rules, with at the root of the tree S and all nodes are inferences. The length of a proof |π| is the number of inferences in π, excluding PR and PL [7, Definition 2].

3.1

Expansions and LKE

Expansion trees are a simple representation of proofs. In a classical proof the substitutions used are the key element of a proof. These are the terms in the ∃R and ∀L inference steps. Expansion trees make the substitutions explicit, but the order of the inferences are omitted. Due to their compact representation, expansions are well suited for transformations. [8] Definition 8. Expansions [7, Definition 4] • ⊥ is an expansion • > is an expansion 8

• P (t1 , . . . , tn ) where P is a predicate with arity n and ti are terms • ¬E where E is an expansion • (E1 ∨ E2 ) where E1 and E2 are expansions • (E1 ∧ E2 ) where E1 and E2 are expansions • (E1 → E2 ) where E1 and E2 are expansions • ∃xA +t1 E1 + · · · +tn En is an expansion where A is a formula and Ei are expansions • ∀xA +t1 E1 + · · · +tn En is an expansion where A is a formula and Ei are expansions The + operator is commutative. A term t in an expansion A +t E is called a selected term. The shallow function maps expansions to formulas [8]. It will, for example, be used to convert a proof from LKE to LK in section 5.7. Sh(>) = > Sh(⊥) = ⊥ Sh(P (t1 , . . . , tn )) = P (t1 , . . . , tn ) Sh(¬E) = ¬Sh(E) Sh(E1 ∨ E2 ) = Sh(E1 ) ∨ Sh(E2 ) Sh(E1 ∧ E2 ) = Sh(E1 ) ∧ Sh(E2 ) Sh(E1 → E2 ) = Sh(E1 ) → Sh(E2 ) t1

Sh(∀xA + E1 · · · +tn En ) = ∀xA Sh(∃xA +t1 E1 · · · +tn En ) = ∃xA For a sequence Γ = E1 , . . . , En its shallow form Sh(Γ) = Sh(E1 ), . . . , Sh(En ). For a sequent Γ ` ∆ its shallow form Sh(Γ ` ∆) = Sh(Γ) ` Sh(∆). Definition 9. Expansion of a formula [7, Definition 4] • ⊥ is an expansion of every formula • > is a dual expansion of every formula • P (t1 , . . . , tn ) is a (dual) expansion of P (t1 , . . . , tn ) • ¬E is a dual expansion of ¬A when E is an expansion of A • ¬E is an expansion of ¬A when E is a dual expansion of A • E1 ∨ E2 is an (dual) expansion of A1 ∨ A2 when E1 and E2 are (dual) expansions of A1 and A2 • E1 ∧ E2 is an (dual) expansion of A1 ∧ A2 when E1 and E2 are (dual) expansions of A1 and A2 • E1 → E2 is an expansion of A1 → A2 when E1 is a dual expansion of A1 and E2 is an expansion of A2 • E1 → E2 is a dual expansion of A1 → A2 when E1 is an expansion of A1 and E2 is a dual expansion of A2 • ∃xA +t1 E1 + · · · +tn En is an expansion of ∃xA when Ei are expansions of A [x := ti ] • ∃xA +f (t1 ,...,tn ) E is a dual expansion of ∃xA when E is a dual expansion of A [x := f (t1 , . . . , tn )] • ∀xA +t1 E1 + · · · +tn En is a dual expansion of ∀xA when Ei are dual expansions of A [x := ti ] • ∀xA +f (t1 ,...,tn ) E is an expansion of ∀xA when E is an expansion of A [x := f (t1 , . . . , tn )]

9

Definition 10. LKE [7, Definition 8]

E, Γ ` ∆, E

I

Γ ` ∆, E ¬L ¬E, Γ ` ∆

E, Γ ` ∆ ¬R Γ ` ∆, ¬E

E1 , Γ ` ∆ E2 , Γ ` ∆ ∨L E1 ∨ E2 , Γ ` ∆

Γ ` ∆, E1 , E2 ∨R Γ ` ∆, E1 ∨ E2

E1 , E2 , Γ ` ∆ ∧L E1 ∧ E2 , Γ ` ∆

Γ ` ∆, E1 Γ ` ∆, E2 ∧R Γ ` ∆, E1 ∧ E2

Γ ` ∆, E1 E2 , Γ ` ∆ →L E1 → E2 , Γ ` ∆

E1 , Γ ` ∆, E2 →R Γ ` ∆, E1 → E2

E, Γ ` ∆ ∃xA + E, Γ ` ∆ E, ∀xA + ω, Γ ` ∆ 0

Γ ` ∆, ∃xA + ω, E

∃Lt0

t0

∀xA +t E + ω, Γ ` ∆

0

Γ ` ∆, ∃xA +t E + ω Γ ` ∆, E

∀Lt

0

Γ ` ∆, ∀xA +t E

Ei , E1 , . . . , Ei−1 , Ei+1 , . . . , En ` ∆ PLi E1 , . . . , E n ` ∆

∃Rt

∀Rt0

Γ ` E1 , . . . , Ei−1 , Ei+1 , . . . , En , Ei PRi Γ ` E1 , . . . , E n

t0 does not occur in A,Sh(Γ) nor Sh(∆). The Skolem terms of an expansion SkTerms(E) is the set of selected terms at its strong quantifiers. SkTermsβ (⊥) = ∅ SkTermsβ (>) = ∅ SkTermsβ (P (t1 , . . . , tn )) = ∅ SkTerms+ (¬E) = SkTerms− (E) SkTerms− (¬E) = SkTerms+ (E) SkTermsβ (E1 ∨ E2 ) = SkTermsβ (E1 ) ∪ SkTermsβ (E2 ) SkTermsβ (E1 ∧ E2 ) = SkTermsβ (E1 ) ∪ SkTermsβ (E2 ) SkTerms+ (E1 → E2 ) = SkTerms− (E1 ) ∪ SkTerms+ (E2 ) SkTerms− (E1 → E2 ) = SkTerms+ (E1 ) ∪ SkTerms− (E2 ) SkTerms+ (∃xA +t1 E1 · · · +tn En ) = SkTerms+ (E1 ) ∪ · · · ∪ SkTerms+ (En ) SkTerms− (∃xA +f (t1 ,...,tn ) E) = {f (t1 , . . . , tn )} ∪ SkTerms− (E) SkTerms+ (∀xA +f (t1 ,...,tn ) E) = {f (t1 , . . . , tn )} ∪ SkTerms+ (E) SkTerms− (∀xA +t1 E1 · · · +tn En ) = SkTerms− (E1 ) ∪ · · · ∪ SkTerms− (En )

For a expansion sequent S 0 = E1 , . . . , En ` F1 , . . . Fm its Skolem terms SkTerms(S) = SkTerms− (E1 ) ∪ · · · ∪ SkTerms− (En ) ∪ SkTerms+ (F1 ) ∪ · · · ∪ SkTerms+ (Fn ) Definition 11. The union of two expansions E1 ∪ E2 is a partial operator defined as [7, Definition 7] 10

• If E1 = ⊥ or E1 = > then E1 ∪ E2 = E2 • If E2 = ⊥ or E2 = > then E1 ∪ E2 = E1 • If E1 = ¬E10 and E2 = ¬E20 then E1 ∪ E2 = ¬(E10 ∪ E20 ) • If E1 = E10 ∨ E100 and E2 = E20 ∨ E200 then E1 ∪ E2 = (E10 ∪ E20 ) ∨ (E100 ∪ E200 ) • If E1 = E10 ∧ E100 and E2 = E20 ∧ E200 then E1 ∪ E2 = (E10 ∪ E20 ) ∧ (E100 ∪ E200 ) • If E1 = E10 → E100 and E2 = E20 → E200 then E1 ∪ E2 = (E10 ∪ E20 ) → (E100 ∪ E200 ) • If E1 = ∃xA +t1 E1,1 · · · +tk E1,k +s1 F1 · · · +sl Fl and E2 = ∃xA +t1 E2,1 · · · +tk E2,k +r1 G1 · · · +rm Gm and {s1 , . . . , sl } ∩ {r1 , . . . , rm } = ∅ then E1 ∪ E2 = ∃xA +t1 (E1,1 ∪ E2,1 ) · · · +tk (E1,k ∪ E2,k ) +s1 F1 · · · +sl Fl +r1 G1 · · · +rm Gm • If E1 = ∀xA +t1 E1,1 · · · +tk E1,k +s1 F1 · · · +sl Fl and E2 = ∀xA +t1 E2,1 · · · +tk E2,k +r1 G1 · · · +rm Gm and {s1 , . . . , sl } ∩ {r1 , . . . , rm } = ∅ then E1 ∪ E2 = ∀xA +t1 (E1,1 ∪ E2,1 ) · · · +tk (E1,k ∪ E2,k ) +s1 F1 · · · +sl Fl +r1 G1 · · · +rm Gm • For all other cases E1 ∪ E2 is undefined For sequences of expansions Γ1 = E1 , . . . , En and Γ2 = F1 , . . . , Fn their union is Γ1 ∪ Γ2 = E1 ∪ F1 , . . . , En ∪ Fn

3.2

Example of an expansion

The following expansion is an expansion of the drinker paradox. ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥)   +a > → ∀yP (y) +f0 (a)) P (f0 (a)) From this expansion a proof of the Skolemized drinker paradox can be constructed, x has to be substituted by a and f0 (a), and y by f0 (a).

11

Chapter 4

Structural Skolemization Skolemization (and its dual Herbrandization) comes in two forms, structural and prefix Skolemization. In structural Skolemization the universal quantifiers are in place replaced by Skolem functions. Prefix Skolemization first puts the formula in prenex normal form and then replaces the quantifiers by the same method as structural Skolemization. Structural Skolemization has the advantage that it is unique up to renaming of the Skolem terms. Prefix is not unique, since there is in general no unique prenex normal form. Also structural Skolemization has fewer arguments in the Skolem terms as prenex normal form moves quantifiers outwards. [3] Structural Skolemization removes all strong quantifiers, ∀ in positive context and ∃ in negative context. The number of strong quantifiers in a formula A is denoted as qocc+ (A). qoccβ (P (t1 , . . . , tn )) = 0 qocc+ (¬A) = qocc− (A) qocc− (¬A) = qocc+ (A) qoccβ (A1 ∨ A2 ) = qoccβ (A1 ) + qoccβ (A2 ) qoccβ (A1 ∧ A2 ) = qoccβ (A1 ) + qoccβ (A2 ) qocc+ (A1 → A2 ) = qocc− (A1 ) + qocc+ (A2 ) qocc− (A1 → A2 ) = qocc+ (A1 ) + qocc− (A2 ) qocc+ (∃xA) = qocc+ (A) qocc− (∃xA) = 1 + qocc− (A) qocc+ (∀xA) = 1 + qocc+ (A) qocc− (∀xA) = qocc− (A)

+,0 −,0 For a formula A its structural Skolemization A0 = skhi (A) in positive context and A0 = skhi (A) in negative context.

12

skβ,n µ (P (t1 , . . . , tm )) = P (t1 , . . . , tm ) −,n sk+,n µ (¬A) = ¬skµ (A) +,n sk−,n µ (¬A) = ¬skµ (A) 0

β,n β,n skβ,n (A2 ) when n0 = n + qoccβ (A1 ) µ (A1 ∨ A2 ) = skµ (A1 ) ∨ skµ 0

β,n β,n skβ,n (A2 ) when n0 = n + qoccβ (A1 ) µ (A1 ∧ A2 ) = skµ (A1 ) ∧ skµ 0

−,n +,n sk+,n (A2 ) when n0 = n + qocc− (A1 ) µ (A1 → A2 ) = skµ (A1 ) → skµ 0

+,n −,n sk−,n (A2 ) when n0 = n + qocc+ (A1 ) µ (A1 → A2 ) = skµ (A1 ) → skµ +,n sk+,n µ1 ,...,µl (∃xA) = ∃x skµ1 ,...,µl ,x (A) 0

+,n 0 sk−,n µ1 ,...,µl (∃xA) = skµ1 ,...,µl (A [x := fn (µ1 , . . . , µl )]) when n = n + 1 0

+,n 0 sk+,n µ1 ,...,µl (∀xA) = skµ1 ,...,µl (A [x := fn (µ1 , . . . , µl )]) when n = n + 1 +,n sk−,n µ1 ,...,µl (∀xA) = ∀x skµ1 ,...,µl ,x (A)

The structural Skolemization of a sequent S = A1 , . . . , An ` B1 , . . . , Bm is A01 , . . . , A0n ` B10 , . . . , Bm +,0 0 • with B10 , . . . , Bm = skhi (B1 ∨ · · · ∨ Bm ) if n = 0

• with A01 , . . . , A0n = sk−,0 hi (A1 ∧ · · · ∧ An ) if m = 0 0 • with A01 , . . . , A0n → B10 , . . . , Bm = sk+,0 hi (A1 ∧ · · · ∧ An → B1 ∨ · · · ∨ Bm ) if n > 0 and m > 0

4.1

Example of Skolemization

The structural Skolemization S 0 of the drinker paradox, S = ` ∃x(P (x) → ∀yP (y)) sk+,0 hi (∃x(P (x) → ∀yP (y))) = +,0 ∃x skhxi (P (x) → ∀yP (y)) =  +,0 ∃x sk−,0 (P (x)) → sk (∀yP (y)) = hxi hxi   +,0 ∃x P (x) → skhxi (∀yP (y)) =   +,1 ∃x P (x) → skhxi (P (f0 (x)) =



∃x (P (x) → P (f0 (x))) S 0 = ` ∃x P (x) → P (f0 (x))

13

Chapter 5

Proof deskolemization In this section the actual algorithm is presented. The four steps of the deskolemization process are in the next sections. Each section is followed by example on the drinker paradox.

5.1

Expansion extraction

The first step in the deskolemization is the extraction of the tautological expansion from the proof in LK. The resulting expansion represents the proof in a simpler form. The extraction function e is recursively defined [7, Lemma 2]. For an axiom   e A, Γ ` ∆, A = A, >, . . . , > ` ⊥, . . . , ⊥, A

Note that formulas that are irrelevant for the axiom inference are substituted by > and ⊥. This reduces the size of the resulting expansion and the complexity of the proof deskolemization process. After the deskolemization step > and ⊥ are substituted by the correct formula’s in section 5.7. For the inference rules ! φ e

Γ ` ∆, A ¬L ¬A, Γ ` ∆

= ¬E, Γ0 ` ∆0

where Γ0 ` ∆0 , E = e e



! φ = Γ0 ` ∆0 , ¬E A, Γ ` ∆ ¬R Γ ` ∆, ¬A  where E, Γ0 ` ∆0 = e

14

 φ Γ ` ∆, A

 φ A, Γ ` ∆

! φ1 φ2 e A, Γ ` ∆ = E1 ∨ E2 , Γ01 ∪ Γ02 ` ∆01 ∪ ∆02 B, Γ ` ∆ ∨L A ∨ B, Γ ` ∆   φ1 where E1 , Γ01 ` ∆01 = e and A, Γ ` ∆   φ2 E2 , Γ02 ` ∆02 = e B, Γ ` ∆ ! φ e = Γ0 ` ∆0 , E1 ∨ E2 Γ ` ∆, A, B ∨R Γ ` ∆, A ∨ B   φ where Γ0 ` ∆0 , E1 , E2 = e Γ ` ∆, A, B ! φ e = E1 ∧ E2 , Γ0 ` ∆0 A, B, Γ ` ∆ ∧L A ∧ B, Γ ` ∆   φ where E1 , E2 , Γ0 ` ∆0 = e A, B, Γ ` ∆ ! φ1 φ2 e Γ ` ∆, A = Γ01 ∪ Γ02 ` ∆01 ∪ ∆02 , E1 ∧ E2 Γ ` ∆, B ∧R Γ ` ∆, A ∧ B   φ1 and where Γ01 ` ∆01 , E1 = e Γ ` ∆, A   φ2 Γ02 ` ∆02 , E2 = e Γ ` ∆, B ! φ1 φ2 e Γ ` ∆, A = E1 → E2 , Γ01 ∪ Γ02 ` ∆01 ∪ ∆02 B, Γ ` ∆ →L A → B, Γ ` ∆   φ1 and where Γ01 ` ∆01 , E1 = e Γ ` ∆, A   φ2 E2 , Γ02 ` ∆02 = e B, Γ ` ∆ ! φ e = Γ0 ` ∆0 , E1 → E2 A, Γ ` ∆, B →R Γ ` ∆, A → B   φ where E1 , Γ0 ` ∆0 , E2 = e A, Γ ` ∆, B

For ∃Ly and ∀Ry the function e is undefined as these inferences can not occur in a proof of a Skolemized formula.

15

e

e

! φ e A [x := y] , Γ ` ∆ is undefined ∃Ly ∃xA, Γ ` ∆ ! φ  = Γ0 ` ∆0 , E1 ∪ ∃xA +t E2 Γ ` ∆, ∃xA, A [x := t] ∃Rt Γ ` ∆, ∃xA   φ where Γ0 ` ∆0 , E1 , E2 = e Γ ` ∆, ∃xA, A [x := t] ! φ  = E1 ∪ ∀xA +t E2 , Γ0 ` ∆0 A [x := t] , ∀xA, Γ ` ∆ ∀Lt ∀xA, Γ ` ∆   φ where E2 , E1 , Γ0 ` ∆0 = e A [x := t] , ∀xA, Γ ` ∆ ! φ e Γ ` ∆, A [x := y] is undefined ∀Ry Γ ` ∆, ∀xA

e

! φ = Γ01 , E, Γ02 ` ∆0 A, Γ1 , Γ2 ` ∆ PL Γ1 , A, Γ2 ` ∆ where E, Γ01 , Γ02 ` ∆0 = e

e



! φ = Γ0 ` ∆01 , E, ∆02 Γ ` ∆1 , ∆2 , A PR Γ ` ∆1 , A, ∆2  where Γ0 ` ∆01 , ∆02 , E = e

5.2

 φ A, Γ1 , Γ2 ` ∆

 φ Γ ` ∆1 , ∆ 2 , A

Example of expansion extraction

Applying the extraction e on the proof π from 2.1 gives   e P (f0 (a)), P (a) ` ∃x(P (x) → P (f0 (x))), P (f0 (f0 (a))), P (f0 (a)) = P (f0 (a)), > ` ⊥, ⊥, P (f0 (a))   φ e = P (f0 (a)), > ` P (f0 (a)), ⊥, ⊥ P (f0 (a)), P (a) ` P (f0 (a)), ∃x(P (x) → P (f0 (x))), P (f0 (f0 (a)))   φ = e P (a) ` P (f0 (a)), ∃x(P (x) → P (f0 (x))), P (f0 (a)) → P (f0 (f0 (a))) > `P (f0 (a)), ⊥, P (f0 (a)) → ⊥

e



  φ = Γ0 ` ∆0 , E1 ∪ ∃xA +t E2 P (a) ` P (f0 (a)), ∃x(P (x) → P (f0 (x))) where Γ0 ` ∆0 , E1 , E2 = > ` P (f0 (a)), ⊥, P (f0 (a)) → ⊥  = > ` P (f0 (a)), ⊥ ∪ ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥  = > ` P (f0 (a)), ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥

16

  φ = > ` ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥ , P (f0 (a)) P (a) ` ∃x(P (x) → P (f0 (x))), P (f0 (a))    φ e = ` ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥ , > → P (f0 (a)) ` ∃x(P (x) → P (f0 (x))), P (a) → P (f0 (a))    φ = Γ0 ` ∆0 , E1 ∪ ∃xA +t E2 e ` ∃x(P (x) → P (f0 (x)))  where Γ0 ` ∆0 , E1 ,E2 = ` ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥ , > → P (f0 (a))  = ` ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥ ∪ e



(∃x(P (x) → P (f0 (x))) +a > → P (f0 (a))) = ` ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥ +a > → P (f0 (a)) Thus the Skolemized expansion is E 0 =` ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥ +a > → P (f0 (a)).

5.3

Skolemized expansion to deskolemized expansion

Now that the proof is in expansion form, it can be easily deskolemized. The strong ∃ and ∀ quantifiers, removed by the Skolemization, have to be restored at the correct place. The Skolem terms corresponding to these strong quantifiers are added as a selected term. The selected term is f (s1 , . . . , sn ) where f is the Skolem functions for the strong quantifier and s1 , . . . , sn are the selected terms in its scope. The process is similar to that of the Skolemization. In the Skolemization, sk, the quantified variables ∀x are recorded to create the correct function. During the deskolemization here the actual selected terms, si , are kept to create the correct Skolem term. The selected terms +t will still contain Skolem functions, these will be replaced by fresh terms in section 5.7. [7, Lemma 3] deskβ,m s1 ,...,sn (A, >) = > deskβ,m s1 ,...,sn (A, ⊥) = ⊥ 0 0 0 0 deskβ,m s1 ,...,sn (P (t1 , . . . , tn ), P (t1 , . . . , tn )) = P (t1 , . . . , tn ) −,m desk+,m s1 ,...,sn (¬A, ¬E) = ¬desks1 ,...,sn (A, E) +,m desk−,m s1 ,...,sn (¬A, ¬E) = ¬desks1 ,...,sn (A, E) 0

β,m β,m deskβ,m s1 ,...,sn (A1 ∨ A2 , E1 ∨ E2 ) = desks1 ,...,sn (A1 , E1 ) ∨ desks1 ,...,sn (A2 , E2 )

when m0 = m + qoccβ (A1 ) 0

β,m β,m deskβ,m s1 ,...,sn (A1 ∧ A2 , E1 ∧ E2 ) = desks1 ,...,sn (A1 , E1 ) ∧ desks1 ,...,sn (A2 , E2 )

when m0 = m + qoccβ (A1 ) 0

+,m −,m desk+,m s1 ,...,sn (A1 → A2 , E1 → E2 ) = desks1 ,...,sn (A1 , E1 ) → desks1 ,...,sn (A2 , E2 )

when m0 = m + qocc+ (A1 ) 0

+,m −,m desk−,m s1 ,...,sn (A1 → A2 , E1 → E2 ) = desks1 ,...,sn (A1 , E1 ) → desks1 ,...,sn (A2 , E2 )

when m0 = m + qocc− (A1 ) 0 t1 tn tn desk+,m En ) = ∃xA +t1 desk+,m desk+,m s1 ,...,sn ,t1 (A [x := t1 ] , E1 ) · · · + s1 ,...,sn ,tn (A [x := tn ] , En ) s1 ,...,sn (∃xA, ∃xA + E1 · · · + 0

fm (s1 ,...,sn ) desk−,m desk−,m s1 ,...,sn (∃xA, E) = ∃xA + s1 ,...,sn (A [x := fm (s1 , . . . , sn )] , E)

when m0 = m + 1 0

fm (s1 ,...,sn ) desk+,m desks+,m (A [x := fm (s1 , . . . , sn )] , E) s1 ,...,sn (∀xA, E) = ∀xA + 1 ,...,sn

when m0 = m + 1 0 t1 tn tn desk−,m En ) = ∀xA +t1 desk−,m desk−,m s1 ,...,sn ,t1 (A [x := t1 ] , E1 ) · · · + s1 ,...,sn ,tn (A [x := tn ] , En ) s1 ,...,sn (∀xA, ∀xA + E1 · · · +

17

The deskolemization of an expansion sequent E1 , . . . , En ` F1 , . . . , Fm for a sequent S = A1 , . . . , An ` B1 , . . . , Bm is desk− (A1 , E1 ), . . . , desk− (An , En ) ` desk+ (B1 , F1 ), . . . , desk+ (Bm , Fm )

5.4

Example of expansion deskolemization

The deskolemized expansion E is desk+ (∃x(P (x) → ∀yP (y)), ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥ +a > → P (f0 (a))) = ∃x(P (x) → ∀yP (y)) +f0 (a) desk+ (P (f0 (a)) → ∀yP (y)), P (f0 (a)) → ⊥) +a desk+ (P (a) → ∀yP (y)), > → P (f0 (a))) desk+ (P (f0 (a)) → ∀yP (y)), P (f0 (a)) → ⊥) = desk− (P (f0 (a)), P (f0 (a))) → desk+ (∀yP (y), ⊥) = P (f0 (a)) → ⊥ desk+ (P (a) → ∀yP (y)), > → P (f0 (a))) = desk− (P (a), >) → desk+ (∀yP (y), P (f0 (a))) = > → ∀yP (y) +f0 (a)) desk+ (P (f0 (a)), P (f0 (a))) = > → ∀yP (y) +f0 (a)) P (f0 (a)) desk+ (∃x(P (x) → ∀yP (y)), ∃x(P (x) → P (f0 (x))) +f0 (a) P (f0 (a)) → ⊥ +a > → P (f0 (a))) =   ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) +a > → ∀yP (y) +f0 (a)) P (f0 (a))

5.5

Proof in LKE from deskolemized expansion

In this section the proof is reconstructed from the expansion. The key point is that the selected terms in the expansions do not have an explicit order. For the ∃Rt and ∀Lt rules the terms may not be in the SkTerms(). This ensures the correct ordering, and the eigenvariable restrictions for the inferences rules.[7, Lemma 6] First, the definition of two helper functions that handle the correct permutation inferences. permLi ((Ei , Γ ` ∆) , π) = π permLi ((Γ1 , Ei , Γ2 ` ∆) , π) =

π PLi Γ1 , Ei , Γ2 ` ∆

permRi ((Γ ` ∆, Ei ) , π) = π permRi ((Γ ` ∆1 , Ei , ∆2 ) , π) =

π PRi Γ ` ∆1 , Ei , ∆2

The actual reconstruction of the proof is done by Pr. It takes an expansion sequent as input and produces a proof in LKE by recursion. Pr is not uniquely defined, yet every possible branch will result in a correct proof. For example A ∧ B ` A ∨ B matches the cases for E1 ∧ E2 and E1 ∨ E2 .

18

 Pr (Γ1 , Ei , Γ2 ` ∆1 , Ej , ∆2 ) = permLi (Γ1 , Ei , Γ2 ` ∆1 , Ej , ∆2 ) , permRj (Ei , Γ1 , Γ2 ` ∆1 , Ej , ∆2 ) , Ei , Γ1 , Γ2 ` ∆1 , ∆2 , Ej





when E = Ei = Ej   Pr (Γ1 , Γ2 ` ∆, E) Pr (Γ1 , Ei , Γ2 ` ∆) = permLi (Γ1 , Ei , Γ2 ` ∆) , ¬L Ei , Γ1 , Γ2 ` ∆ when Ei = ¬E   Pr (E, Γ ` ∆1 , ∆2 ) Pr (Γ ` ∆1 , Ei , ∆2 ) = permLi (Γ ` ∆1 , Ei , ∆2 ) , ¬R Γ ` ∆1 , ∆2 , Ei when Ei = ¬E   Pr (E1 , Γ1 , Γ2 ` ∆) Pr (E2 , Γ1 , Γ2 ` ∆) Pr (Γ1 , Ei , Γ2 ` ∆) = permLi (Γ1 , Ei , Γ2 ` ∆) , ∨L Ei , Γ1 , Γ2 ` ∆ when Ei = E1 ∨ E2   Pr (Γ ` ∆1 , ∆2 , E1 , E2 ) Pr (Γ ` ∆1 , Ei , ∆2 ) = permLi (Γ ` ∆1 , Ei , ∆2 ) , ∨R Γ ` ∆1 , ∆2 , Ei when Ei = E1 ∨ E2   Pr (E1 , E2 , Γ1 , Γ2 ` ∆) Pr (Γ1 , Ei , Γ2 ` ∆) = permLi (Γ1 , Ei , Γ2 ` ∆) , ∧L Ei , Γ1 , Γ2 ` ∆ when Ei = E1 ∧ E2   Pr (Γ ` ∆1 , ∆2 , E1 ) Pr (Γ ` ∆1 , ∆2 , E2 ) Pr (Γ ` ∆1 , Ei , ∆2 ) = permLi (Γ ` ∆1 , Ei , ∆2 ) , ∧R Γ ` ∆1 , ∆2 , Ei when Ei = E1 ∧ E2   Pr (Γ1 , Γ2 ` ∆, E1 ) Pr (E2 , Γ1 , Γ2 ` ∆) Pr (Γ1 , Ei , Γ2 ` ∆) = permLi (Γ1 , Ei , Γ2 ` ∆) , →L Ei , Γ1 , Γ2 ` ∆ when Ei = E1 → E2   Pr (E1 , Γ ` ∆1 , ∆2 , E2 ) Pr (Γ ` ∆1 , Ei , ∆2 ) = permLi (Γ ` ∆1 , Ei , ∆2 ) , →R Γ ` ∆1 , ∆2 , Ei when Ei = E1 → E2   Pr (E, Γ1 , Γ2 ` ∆) Pr (Γ1 , Ei , Γ2 ` ∆) = permLi (Γ1 , Ei , Γ2 ` ∆) , ∃Lf (t¯) Ei , Γ1 , Γ2 ` ∆ ¯

when Ei = ∃xA +f (t) E   Pr (Γ ` ∆1 , ∆2 , ∃xA + ω, E) Pr (Γ ` ∆1 , Ei , ∆2 ) = permLi (Γ ` ∆1 , Ei , ∆2 ) , ∃Rt Γ ` ∆1 , ∆2 , Ei when Ei = ∃xA +t E + ω and t 6∈ SkTerms(Γ ` ∆1 , Ei , ∆2 )   Pr (E, ∀xA + ω, Γ ` ∆) Pr (Γ1 , Ei , Γ2 ` ∆) = permLi (Γ1 , Ei , Γ2 ` ∆) , ∀Lt Ei , Γ1 , Γ2 ` ∆ t when Ei = ∀xA + E + ω and t 6∈ SkTerms(Γ1 , Ei , Γ2 ` ∆)   Pr (Γ, ` ∆1 , ∆2 , E) Pr (Γ ` ∆1 , Ei , ∆2 ) = permLi (Γ ` ∆1 , Ei , ∆2 ) , ∀Rf (t¯) Γ ` ∆1 , ∆2 , Ei ¯

when Ei = ∀xA +f (t) E

19

Example of proof construction in LKE

5.6

From the previous section we have ` ∃x(P (x) → ∀yP (y))+f0 (a) (P (f0 (a)) → ⊥)+a > → ∀yP (y) +f0 (a)) P (f0 (a)) to construct the proof we simply apply Pr.    Pr ` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) +a > → ∀yP (y) +f0 (a)) P (f0 (a)) Only the rule ∃ at the right matches, with t = f0 (a) or t = a. However f0 (a) ∈ SkTerms(S) = f0 (a) since SkTerms+ (∀yP (y) +f0 (a)) P (f0 (a))) = f0 (a). Thus the first step is ∃Ra .  Pr ` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) , > → ∀yP (y) +f0 (a)) P (f0 (a))  ∃Ra ` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) +a > → ∀yP (y) +f0 (a)) P (f0 (a)) The next possible step is →R, since ∃Rf0 (a) is still in SkTerms() and can not be applied. The final result of Pr is P (f0 (a)), > ` ∃x(P (x) → ∀yP (y)), ⊥, P (f0 (a)) PR1 P (f0 (a)), > ` P (f0 (a)), ∃x(P (x) → ∀yP (y)), ⊥ →R > ` P (f0 (a)), ∃x(P (x) → ∀yP (y)), (P (f0 (a)) → ⊥) ∃Rf0 (a) > ` P (f0 (a)), ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) PR1 > ` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) , P (f0 (a)) > ` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) , ∀yP (y) +f0 (a)) P (f0 (a))

∀Rf0 (a)

` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) , > → ∀yP (y) +f0 (a)) P (f0 (a))

→R

 ∃Ra ` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) +a > → ∀yP (y) +f0 (a)) P (f0 (a))

LKE to LK

5.7

The proof generated is not yet a proof in LK. The sequents are made from expansions and not formulas, the terms in for example ∃R may have Skolem functions. The Skolem terms are removed in the first step [7, Lemma 7]  rm Γ ` ∆ = Sh(Γ ` ∆)  π  rm (π) rm Γ ` ∆ R = R Sh(Γ ` ∆) when R ∈ {¬L, ¬R, ∨R, ∧L, →R, ∃Rx , ∀Ly , PLn , PRm }  π  π2 rm (π1 ) rm (π2 ) 1 R = rm when R ∈ {∨L, ∧R, →L} R Γ`∆ Sh(Γ ` ∆)   π rm(π [f (t¯) := y]) rm ∃L = ∃Ly ¯ ¯ f (t) f (t) ∃xA, Sh(Γ) ` Sh(∆) ∃xA + E, Γ ` ∆  rm

π ∀Rf (t¯) Γ ` ∆, ∀xA +f (t¯) E



when y does not occur in ∃xA, Sh(Γ) ` Sh(∆) rm(π [f (t¯) := y]) = ∀Ry Sh(Γ) ` Sh(∆), ∀xA when y does not occur in Sh(Γ) ` Sh(∆), ∀xA

20



The final step is to remove > and ⊥ from the formulas. This is simply done by reconstructing the proof by applying the inference steps.   rmTF (A, Γ ` ∆, A) , A, >, . . . , > ` ⊥, . . . , ⊥, A = A, Γ ` ∆, A   π rmTF((Γ0 ` ∆0 ), π) rmTF (Γ ` ∆) , S R = R Γ`∆ 0 0 when Γ ` ∆ R Γ`∆   π1 π2 rmTF((Γ0 ` ∆0 ), π1 ) rmTF((Γ00 ` ∆00 ), π2 ) R = rmTF (Γ ` ∆) , R S Γ`∆ 0 0 00 00 Γ `∆ when Γ ` ∆ R Γ`∆

Now the deskolemization process is completed. An expansion was extracted, e, deskolemized, desk, a proof was reconstructed, Pr and finally rewritten as a proof in LK by rm and rmTF. The appendix A lists an actual implementation in Haskell of the described deskolemization process.

5.8

Example of LKE to LK

Applying rm to the generated proof is simple. In most cases only Sh is needed, which turns the expansions into formulas. The first step is as follows  rm

π  ∃Ra f0 (a) ` ∃x(P (x) → ∀yP (y)) + (P (f0 (a)) → ⊥) +a > → ∀yP (y) +f0 (a)) P (f0 (a))

 =

rm (π)  ∃Ra = Sh(` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) +a > → ∀yP (y) +f0 (a)) P (f0 (a)) ) rm (π) ∃Ra = ` ∃x(P (x) → ∀yP (y))

The next step for the ⇒R inference rule is similar. For the third step at the inference rule ∀Rf0 (a) a fresh variable is needed, for example x2 . All occurrences of f0 (a) in the proof have to be substituted by x2 because of rm(π [f (t¯) := y]). Thus P (f0 (a)), > ` ∃x(P (x) → ∀yP (y)), ⊥, P (f0 (a)) PR1 P (f0 (a)), > ` P (f0 (a)), ∃x(P (x) → ∀yP (y)), ⊥ →R > ` P (f0 (a)), ∃x(P (x) → ∀yP (y)), (P (f0 (a)) → ⊥) ∃Rf0 (a) > ` P (f0 (a)), ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) PR1 > ` ∃x(P (x) → ∀yP (y)) +f0 (a) (P (f0 (a)) → ⊥) , P (f0 (a)) becomes P (x2 ), > ` ∃x(P (x) → ∀yP (y)), ⊥, P (x2 ) PR1 P (x2 ), > ` P (x2 ), ∃x(P (x) → ∀yP (y)), ⊥ →R > ` P (x2 ), ∃x(P (x) → ∀yP (y)), (P (x2 ) → ⊥) ∃Rx2 > ` P (x2 ), ∃x(P (x) → ∀yP (y)) +x2 (P (x2 ) → ⊥) PR1 > ` ∃x(P (x) → ∀yP (y)) +x2 (P (x2 ) → ⊥) , P (x2 ) Note that also the inference ∃Rf0 (a) changed to ∃Rx2 . The final result of rm is

21

P (x2 ), > ` ∃x(P (x) → ∀yP (y)), ⊥, P (x2 ) PR1 P (x2 ), > ` P (x2 ), ∃x(P (x) → ∀yP (y)), ⊥ →R > ` P (x2 ), ∃x(P (x) → ∀yP (y)), P (x2 ) → ⊥ ∃Rx2 > ` P (x2 ), ∃x(P (x) → ∀yP (y)) PR1 > ` ∃x(P (x) → ∀yP (y)), P (x2 ) ∀Rx2 > ` ∃x(P (x) → ∀yP (y)), ∀yP (y) →R ` ∃x(P (x) → ∀yP (y)), > → ∀yP (y) ∃Ra ` ∃x(P (x) → ∀yP (y)) The final function to produce the proof in LK is rmTF. This function simply applies the inferences rules starting at the root of the proof. The result of rmTF is P (x2 ), P (a) ` ∃x(P (x) → ∀yP (y)), ∀yP (y)), P (x2 ) PR1 P (x2 ), P (a) ` P (x2 ), ∃x(P (x) → ∀yP (y)), ∀yP (y)) →R P (a) ` P (x2 ), ∃x(P (x) → ∀yP (y)), P (x2 ) → ∀yP (y)) ∃Rx2 P (a) ` P (x2 ), ∃x(P (x) → ∀yP (y)) PR1 P (a) ` ∃x(P (x) → ∀yP (y)), P (x2 ) ∀Rx2 P (a) ` ∃x(P (x) → ∀yP (y)), ∀yP (y) →R ` ∃x(P (x) → ∀yP (y)), P (a) → ∀yP (y) ∃Ra ` ∃x(P (x) → ∀yP (y)) This indeed is a proof of the drinker paradox ` ∃x(P (x) → ∀yP (y)).

22

Chapter 6

Conclusion We have shown an algorithm to deskolemize a proof. The algorithm takes a sequent a proof of the skolemized sequent and produces a proof of the original sequent. The implementation can be found in appendix A. The algorithm works for cut-free proofs. The expansions trees that are extracted from the proof do not support a cut rule. One way to overcome this limitation is to use a cut elimination. However, an extension to expansions trees, expansions trees with cut[6] is a promising result to deskolemization with cut rules.

23

Bibliography [1] Alexandre Riazanov, A. V. The design and implementation of vampire. AI Communications 15 (2002), 91–110. [2] Baaz, M., Hetzl, S., Leitsch, A., Richter, C., and Spohr, H. Cut-elimination: Experiments with ceres. In Logic for Programming, Artificial Intelligence, and Reasoning, F. Baader and A. Voronkov, Eds., vol. 3452 of Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2005, pp. 481–495. [3] Baaz, M., and Leitsch, A. On skolemization and proof complexity. Fundamenta Informaticae 20, 4 (1994), 353–379. [4] Gentzen, G. Untersuchungen u ¨ber das logische schliessen. Mathematische Zeitschrift 39 (1934), 176–210. [5] Gentzen, G. Untersuchungen u ¨ber das logische schliessen. Mathematische Zeitschrift 39 (1934), 405–431. [6] Hetzl, S., and Weller, D. Expansion trees with cut. CoRR abs/1308.0428 (2013). [7] M. Baaz, S. H., and Weller, D. On the complexity of proof deskolemization. The Journal of Symbolic Logic 77, 2 (2012). [8] Miller, D. A. A compact representation of proofs. Studia Logica 46, 4 (1987), 347–370. [9] Pelletier, F., Sutcliffe, G., and Suttner, C. The Development of CASC. AI Communications 15, 2-3 (2002), 79–90. [10] Smullyan, R. M. What is the name of this book? Prentice-Hall Englewood Cliffs, New Jersey, 1978. [11] Sutcliffe, G. The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43, 4 (2009), 337–362. [12] Sutcliffe, G., and Suttner, C. The State of CASC. AI Communications 19, 1 (2006), 35–48.

24

Appendices

25

Appendix A

Haskell implementation The implementation includes a tablaux prover for testing purposes. The core functionality, extract, desk, pr, rm and rmTF can be found in Expansion.hs. Function.hs contains a function sk that implements the Skolemization of a formula.

Formula.hs module Formula ( allVariables , substituteTerm , Formula (..) , Term (..) , Function , Variable ,Predicate , Symbol (..) , Sequent ,substitute ,fnot ,for ,fand ,fimp ,fpred , Proof (..) , LR (..) , Rule (..) , drinkerParadox ,RuleResult ,termsS , freshVariable , freeTerms ) where

import Prelude hiding (Left ,Right) import Data.List import Data.Maybe type Function = String type Variable = String type Predicate = String data Term = Fun Function [Term] | Var Variable deriving (Eq) instance Show Term where show (Var name) = name show (Fun name terms) = name ++ "" ++ (show terms) ++ "" data Symbol = Not | Or | And | Imp | Exists | Forall

deriving (Eq)

instance Show Symbol where show Not = "\xac" show Or = "\x2228 " show And = "\x2227 " show Imp = "\x2192 " show Exists = "\x2203" show Forall = "\x2200"

data Formula = TopBot | Pred Predicate [Term] | Unary Symbol Formula | Binary Symbol Formula Formula | Quantifier Symbol Variable Formula deriving (Eq) instance Show Formula where show (Pred p terms) = p ++

(show terms)

26

show (Unary s f) = show s ++ (show f) show ( Binary s f1 f2) = "(" ++ (show f1) ++ (show s) ++ (show f2) ++ ")" show ( Quantifier s x f) = (show s) ++ x ++ (show f) type Sequent = ([ Formula ],[ Formula ]) ant :: Sequent -> [ Formula ] ant (gamma ,delta) = gamma suc :: Sequent -> [ Formula ] suc (gamma ,delta) = delta data LR = Left | Right deriving (Eq ,Show) data Rule = Axiom | SymbolRule LR Symbol | QuantifierRule LR Symbol Term | Perm LR Int deriving (Show) type RuleResult = (Rule ,[ Sequent ]) data Proof = Proof Rule Sequent [Proof] indent :: Int -> String indent n = ( replicate (n*4) ’ ’) printProof :: (Int ,Proof) -> String printProof (n,( Proof rule s proofs )) = concat (map printProof (zip [n..( length proofs )] proofs )) ++ "\n" ++ ( indent n) ++ " --------------" ++ (show rule) ++ "\n" ++ (show s) instance Show Proof where show proof = printProof (0, proof) breakFormula breakFormula breakFormula breakFormula breakFormula formulaSymbol formulaSymbol formulaSymbol formulaSymbol formulaSymbol

:: Formula -> [ Formula ] (Pred _ _) = [] (Unary s f) = [f] ( Quantifier s _ f) = [f] ( Binary s f1 f2) = [f1 ,f2] :: Formula -> Maybe Symbol (Pred _ _) = Nothing (Unary s _) = Just s ( Quantifier s _ _) = Just s ( Binary s _ _) = Just s

fpred :: String -> [Term] -> Formula fpred s terms = Pred s terms fnot :: Formula -> Formula fnot f = Unary Not f fand :: Formula -> Formula -> Formula fand f1 f2 = Binary And f1 f2 for :: Formula -> Formula -> Formula for f1 f2 = Binary Or f1 f2 fimp :: Formula -> Formula -> Formula fimp f1 f2 = Binary Imp f1 f2 fexists :: Variable -> Formula -> Formula fexists x f = Quantifier Exists x f

27

fforall :: Variable -> Formula -> Formula fforall x f = Quantifier Forall x f -- |A list of all variables x1 , x2 , ... allVariables :: [ Variable ] allVariables = vars 1 where vars :: Int -> [ Variable ] vars n = ("x" ++ show(n)): vars (n+1) freshVariable :: Sequent -> Variable freshVariable (ant ,suc) = head [x | x [Term] freeTerms f = (terms f) \\ ( binderTerms f) binderTerms :: Formula -> [Term] binderTerms f = nub ( binderTerms ’ f) where binderTerms ’ (Pred _ t) = [] binderTerms ’ ( Quantifier Exists x f) = (Var x):( binderTerms f) binderTerms ’ ( Quantifier Forall x f) = (Var x):( binderTerms f) binderTerms ’ (Unary _ f) = terms f binderTerms ’ ( Binary _ f1 f2) = ( binderTerms f1) ++ ( binderTerms f2)

termsS :: Sequent -> [Term] termsS (gamma ,delta) = ( concat $ map terms gamma) ++ ( concat $ map terms delta) terms :: Formula -> [Term] terms f = nub (terms ’ f) where terms ’ (Pred _ t) = t terms ’ ( Quantifier Exists x f) = (Var x):( terms f) terms ’ ( Quantifier Forall x f) = (Var x):( terms f) terms ’ (Unary _ f) = terms f terms ’ ( Binary _ f1 f2) = (terms f1) ++ (terms f2) substituteTerm :: Term -> Term -> Term -> substituteTerm a@(Var _) b t = substituteTerm a@(Fun f terms) x t = Fun f (map (\y -> ( substituteTerm

Term if a == b then t else a if a == x then t else y x t)) terms)

substitute :: Formula -> Term -> Term -> Formula substitute (Pred p terms) var t = Pred p (map (\x -> substituteTerm x var t) terms) substitute err@( Quantifier Exists x f) var t = if (Var x) == var then error ("Oops "++( show var )++" is bound in " ++( show err )) else Quantifier Exists x ( substitute f var t) substitute err@( Quantifier Forall x f) var t = if (Var x) == var then error ("Oops "++( show var )++" is bound in " ++( show err )) else Quantifier Forall x ( substitute f var t) substitute (Unary b f) var t = Unary b ( substitute f var t) substitute ( Binary b f1 f2) var t = Binary b ( substitute f1 var t) ( substitute f2 var t) drinkerParadoxPart :: Formula

28

drinkerParadoxPart = fimp (fpred "p" [Var "x1"]) ( fforall "x2" (fpred "p" [Var "x2"])) drinkerParadox :: Formula drinkerParadox = fexists "x1" ( drinkerParadoxPart ) drinkerParadoxAlmost :: Sequent drinkerParadoxAlmost = ([], [ substitute drinkerParadoxPart (Var "x1") (Var "x"), drinkerParadox ])

29

Expansions.hs module Expansion (Expansion ,extract ,desk ,pr ,sh , skolemTerms ,shS , skolemTermsS , rm ,rmTF) where import Prelude hiding (Left , Right) import import import import import

Formula Prover Data.List Data.Maybe Functions

data Expansion = Top | Bot | Pred Predicate [Term] | Unary Symbol Expansion | Binary Symbol Expansion Expansion | Quantifier Symbol Variable Formula [(Term , Expansion )] deriving (Eq)

instance Show Expansion where show Top = "Top" show Bot = "Bot" show ( Expansion .Pred p terms) = p ++ (show terms) show ( Expansion .Unary s f) = show s ++ (show f) show ( Expansion . Binary s f1 f2) = "(" ++ (show f1) ++ (show s) ++ (show f2) ++ ")" show ( Expansion . Quantifier s x f omega) = (show s) ++ x ++ (show f) ++ "+" ++ (show omega) type ExpSequent = ([ Expansion ],[ Expansion ]) data LKEProof = LKEProof Rule ExpSequent [ LKEProof ] indent :: Int -> String indent n = ( replicate (n*4) ’ ’) printProof :: (Int , LKEProof ) -> String printProof (n,( LKEProof rule s proofs )) = concat (map printProof (zip [n..( length proofs )] proofs )) ++ "\n" ++ ( indent n) ++ " --------------" ++ (show rule) ++ "\n" ++ (show s) instance Show LKEProof where show proof = printProof (0, proof) shS :: ExpSequent -> ExpSequent shS (gamma ,delta) = (map sh gamma ,map sh delta) sh sh sh sh sh sh sh

:: Expansion -> Expansion Top = Top Bot = Bot ( Expansion .Pred p terms) = Expansion .Pred p terms ( Expansion .Unary s e) = Expansion .Unary s (sh e) ( Expansion . Binary s e1 e2) = Expansion . Binary s (sh e1) (sh e2) ( Expansion . Quantifier s x f omega) = Expansion . Quantifier s x f []

skolemTermsS :: ExpSequent -> [Term] skolemTermsS (gamma ,delta) = union ( concat $ map ( skolemTerms False) gamma) ( concat $ map ( skolemTerms True) delta) skolemTerms :: Bool -> Expansion -> [Term] skolemTerms _ Top = []

30

skolemTerms _ Bot = [] skolemTerms _ ( Expansion .Pred _ _) = [] skolemTerms b ( Expansion .Unary Not e) = skolemTerms (not b) e skolemTerms b ( Expansion . Binary And e1 e2) = union ( skolemTerms b e1) ( skolemTerms b e2) skolemTerms b ( Expansion . Binary Or e1 e2) = union ( skolemTerms b e1) ( skolemTerms b e2) skolemTerms b ( Expansion . Binary Imp e1 e2) = union ( skolemTerms (not b) e1) ( skolemTerms b e2) skolemTerms True ( Expansion . Quantifier Exists _ _ omega) = foldl1 union (map ( skolemTerms True) [e | (t,e) (Term , Expansion ) substituteTE (t,e) x t’ | t == x = (t’, esubstitute e x t’) | otherwise = (t, esubstitute e x t’) esubstituteS :: ExpSequent -> Term -> Term -> ExpSequent esubstituteS (gamma ,delta) var t = (map (\x -> esubstitute x var t) gamma , map (\x -> esubstitute x var t) delta) esubstituteP :: LKEProof -> Term -> Term -> LKEProof esubstituteP ( LKEProof ( QuantifierRule lr symbol term) s proofs ) x y = ( LKEProof ( QuantifierRule lr symbol ( substituteTerm term x y)) ( esubstituteS s x y) (map (\p -> esubstituteP p x y) proofs )) esubstituteP ( LKEProof rule s proofs ) x y = ( LKEProof rule ( esubstituteS s x y) (map (\p -> esubstituteP p x y) proofs )) esubstitute :: Expansion -> Term -> Term -> Expansion esubstitute Top _ _ = Top esubstitute Bot _ _ = Bot esubstitute ( Expansion .Pred p terms) var t = Expansion .Pred p (map (\x -> substituteTerm x var t) terms)

31

esubstitute err@( Expansion . Quantifier Exists x f omega) var t = if (Var x) == var then error ("Oops "++( show var )++" is bound in " ++( show err )) else Expansion . Quantifier Exists x ( substitute f var t) omega ’ where omega ’ = [ substituteTE te var t | te ExpSequent extract ( Proof Axiom (a:gamma ,b:delta) proofs ) = ( toExpansion a : replicate ( length gamma) Top , toExpansion b : replicate ( length delta) Bot) extract ( Proof ( SymbolRule Left symbol ) sequent proofs ) = extractLeft symbol (map extract proofs ) extract ( Proof ( SymbolRule Right symbol ) sequent proofs ) = extractRight symbol (map extract proofs ) extract ( Proof (Perm Left n) sequent [proof ]) = ( fromFirst n gamma ’,delta ’) where (gamma ’,delta ’) = extract proof extract ( Proof (Perm Right n) sequent [proof ]) = (gamma ’, fromFirst n delta ’) where (gamma ’,delta ’) = extract proof extract ( Proof ( QuantifierRule Right Exists term) sequent@ (_,f@( Formula . Quantifier Exists x a):_) [proof ]) = (gamma , eunion e1 e2 ’: delta) where (gamma ,e2:e1:delta) = extract proof e2 ’ = Expansion . Quantifier Exists x a [(term ,e2)] eunion eunion eunion eunion eunion eunion

:: Expansion -> Expansion -> Expansion Top e2 = e2 Bot e2 = e2 e1 Top = e1 e1 Bot = e1 ( Expansion .Pred p1 terms1 ) ( Expansion .Pred p2 terms2 ) | and [p1 == p2 , terms1 == terms2 ] = Expansion .Pred p1 terms1 | otherwise = error "No union" eunion ( Expansion .Unary s1 e1) ( Expansion .Unary s2 e2) | s1 == s2 = Expansion .Unary s1 ( eunion e1 e2) | otherwise = error "No union" eunion ( Expansion . Binary s1 e1 e1 ’) ( Expansion . Binary s2 e2 e2 ’) | s1 == s2 = Expansion . Binary s1 ( eunion e1 e2) ( eunion e1 ’ e2 ’) | otherwise = error "No union" eunion ( Expansion . Quantifier s1 x1 a1 e1) ( Expansion . Quantifier s2 x2 a2 e2) | and [s1 == s2 ,x1 == x2 ,a1 == a2] = Expansion . Quantifier s1 x1 a1 (eunion ’ e1 e2) | otherwise = error "No union" where eunion ’ :: [(Term , Expansion )] -> [(Term , Expansion )] -> [(Term , Expansion )]

32

eunion ’ [] b = b eunion ’ (a@(t,e1):as) b | ( elemIndex t bterms ) == Nothing = a:eunion ’ as b | otherwise = (t, eunion e1 e2) : eunion ’ as b where (bterms ,_) = unzip b (t2 ,e2) = b !! ( fromJust ( elemIndex t bterms )) eunion e1 e2 = error $ "No union for " ++ (show e1) ++ " and "++ (show e2) enot :: Expansion -> Expansion enot e = Expansion .Unary Not e eimp :: Expansion -> Expansion -> Expansion eimp e1 e2 = Expansion . Binary Imp e1 e2 extractLeft :: Symbol -> [ ExpSequent ] -> ExpSequent extractLeft Not [( gamma ,e:delta )] = (enot e:gamma ,delta) extractRight :: Symbol -> [ ExpSequent ] -> ExpSequent extractRight Not [(e:gamma ,delta )] = (gamma ,enot e:delta) extractRight Imp [(e1:gamma ,e2:delta )] = (gamma ,eimp e1 e2:delta)

desk desk desk desk

desk desk

desk

desk

desk

:: Bool -> Int -> [Term] -> Formula -> Expansion -> Expansion _ _ _ _ Top = Top _ _ _ _ Bot = Bot _ _ _ f@( Formula .Pred p terms) e@( Expansion .Pred p2 terms2 ) | and [p == p2] = e | otherwise = error (" Predicates don ’t match: " ++ (show f) ++ " " ++ (show e)) b n mu ( Formula .Unary Not f) ( Expansion .Unary Not e) = desk (not b) n mu f e -- TODO check? True n mu ( Formula . Binary Imp f1 f2) ( Expansion . Binary Imp e1 e2) = Expansion . Binary Imp (desk False n mu f1 e1) (desk True m mu f2 e2) where m = n + (qocc False f1) True n mu ( Formula . Quantifier Exists x a) ( Expansion . Quantifier Exists _ _ omega) = ( Expansion . Quantifier Exists x a omega ’) where omega ’ = [(term ,desk True n (mu ++ [term ]) a e) | (term ,e) ExpSequent -> LKEProof -> LKEProof permL 0 _ proof = proof permL index s proof = LKEProof (Perm Left index) s [proof] permR :: Int -> ExpSequent -> LKEProof -> LKEProof permR 0 _ proof = proof permR index s proof = LKEProof (Perm Right index) s [proof] symbolIndex :: Symbol -> [ Expansion ] -> Maybe Int symbolIndex s e = symbolIndex ’ 0 s e where symbolIndex ’ :: Int -> Symbol -> [ Expansion ] -> Maybe Int symbolIndex ’ _ symbol [] = Nothing symbolIndex ’ index symbol (( Expansion . Binary symbol ’ _ _):e) | symbol == symbol ’ = Just index

33

| otherwise = symbolIndex ’ ( index +1) symbol e symbolIndex ’ index symbol (( Expansion .Unary symbol ’ _):e) | symbol == symbol ’ = Just index | otherwise = symbolIndex ’ ( index +1) symbol e symbolIndex ’ index symbol (( Expansion . Quantifier symbol ’ _ _ _):e) | symbol == symbol ’ = Just index | otherwise = symbolIndex ’ ( index +1) symbol e symbolIndex ’ index symbol (_:e) = symbolIndex ’ ( index +1) symbol e pr :: ExpSequent -> LKEProof pr s@(gamma ,delta) | length ( intersect gamma ’ delta ’) > 0 = axiom gamma delta | leftRight == Left = permL index s ( prLeft ( setFirst index gamma ,delta )) | leftRight == Right = permR index s ( prRight (gamma , setFirst index delta )) where gamma ’ = deleteBy (==) Bot ( deleteBy (==) Top gamma) delta ’ = deleteBy (==) Bot ( deleteBy (==) Top delta) axiom gamma delta = let e = head ( intersect gamma ’ delta ’) li = fromJust ( elemIndex e gamma) ri = fromJust ( elemIndex e delta) in permL li (gamma , setFirst ri delta) (permR ri s ( LKEProof Axiom ( setFirst li gamma , setFirst ri delta) [])) (leftRight , index) = head $ catMaybes (map ( hasExpansionOf s) [Or ,And ,Imp ,Forall , Exists ]) prLeft :: ExpSequent -> LKEProof prLeft (( Expansion . Binary Imp e1 e2): gamma ,delta) = LKEProof ( SymbolRule Left Imp) s [pr (gamma ,e1:delta),pr (e2:gamma ,delta )] prLeft (e:gamma ,delta) = error $ "Left " ++ show e prRight :: ExpSequent -> LKEProof prRight (gamma ,( Expansion . Quantifier Exists x a omega ): delta) = LKEProof ( QuantifierRule Right Exists t) s [(pr (gamma ,e:e2:delta ))] where (t,e) = head [(t’,e’) | (t’,e’) Symbol -> Maybe (LR ,Int) hasExpansionOf (gamma ,delta) s | symbolIndex s gamma /= Nothing = Just (Left , fromJust ( symbolIndex s gamma )) | symbolIndex s delta /= Nothing = Just (Right , fromJust ( symbolIndex s delta )) | otherwise = Nothing rm :: LKEProof -> LKEProof rm ( LKEProof Axiom s []) = ( LKEProof Axiom (shS s) [])

34

rm ( LKEProof rule@( SymbolRule lr symbol ) s proofs ) = ( LKEProof rule (shS s) (map rm proofs )) rm ( LKEProof ( QuantifierRule Left Exists term) s [proof ]) = ( LKEProof ( QuantifierRule Left Exists y) ( esubstituteS (shS s) term y) [ esubstituteP (rm proof) term y]) where y = Var ( efreshVariable s) rm ( LKEProof ( QuantifierRule Right Forall term) s [proof ]) = ( LKEProof ( QuantifierRule Right Forall y) ( esubstituteS (shS s) term y) [ esubstituteP (rm proof) term y]) where y = Var ( efreshVariable s) rm ( LKEProof rule@( QuantifierRule _ _ term) s [proof ]) = ( LKEProof rule (shS s) [rm proof ]) rm ( LKEProof rule@(Perm _ _) s [proof ]) = ( LKEProof rule (shS s) [rm proof ]) rm p = error ("Error" ++ (show p)) rmTF :: Sequent -> LKEProof -> Proof rmTF s ( LKEProof Axiom _ []) = Proof Axiom s [] rmTF s ( LKEProof rule _ proofs ) = Proof rule s proofs ’ where (_, nextsequents ) = fromJust $ applyRule s rule r = zip nextsequents proofs proofs ’ = [rmTF s’ p’ | (s’,p’) Formula -> Int b (Pred _ _ ) = 0 b ( Unary Not f) = qocc ( Prelude .not b) f b ( Binary Or f1 f2) = (qocc b f1) + (qocc b f2) b ( Binary And f1 f2) = (qocc b f1) + (qocc b f2) True ( Binary Imp f1 f2) = (qocc False f1) + (qocc True f2) False ( Binary Imp f1 f2) = (qocc True f1) + (qocc False f2) True ( Quantifier Forall x f) = 1 + (qocc True f) False ( Quantifier Forall x f) = qocc False f True ( Quantifier Exists x f) = qocc True f False ( Quantifier Exists x f) = 1 + (qocc False f)

skolemFunc :: Int -> Function skolemFunc n = ("f" ++ (show n)) sequentAsFormula sequentAsFormula sequentAsFormula sequentAsFormula sequentAsFormula

:: Sequent -> Formula ([] ,[]) = error "Empty sequent " ([], delta) = foldl1 for delta (gamma ,[]) = foldl1 fand gamma (gamma ,delta) = fimp ( foldr1 fand gamma ) ( foldr1 for delta)

unfoldFormula :: Int -> Symbol -> Formula -> [ Formula ] unfoldFormula 1 _ f = [f] unfoldFormula n symbol ( Binary symbol ’ f1 f2) | symbol == symbol ’ = f1: unfoldFormula (n -1) symbol f2 | otherwise = error "Wrong symbol " unfoldFormula _ _ f = error $ "Can ’t unfold " ++ (show f)

formulaAsSequent :: Int -> Int -> Formula -> Sequent formulaAsSequent 0 0 _ = error "Empty formula " formulaAsSequent n 0 f = ( unfoldFormula n And f ,[]) formulaAsSequent 0 m f = ([], unfoldFormula m Or f) formulaAsSequent n m ( Binary Imp f1 f2) = ( unfoldFormula n And f1 , unfoldFormula m Or f2) skSequent :: Sequent -> Sequent skSequent s@(ant ,suc) = formulaAsSequent ( length ant) ( length suc) $ sk True 0 [] $ sequentAsFormula s sk sk sk sk sk sk sk

sk

:: Bool -> Int -> [Term] -> Formula -> Formula b n mu f@(Pred _ _) = f b n mu (Unary Not f) = Unary Not (sk (not b) n mu f) b n mu ( Binary Or f1 f2) = Binary Or (sk b n mu f1) (sk b m mu f2) where m = n + (qocc b f1) b n mu ( Binary And f1 f2) = Binary And (sk b n mu f1) (sk b m mu f2) where m = n + (qocc b f1) b n mu ( Binary Imp f1 f2) = Binary Imp (sk (not b) n mu f1) (sk b m mu f2) where m = n + (qocc (not b) f1) True n mu ( Quantifier Forall x f) = sk True m mu f’ where m = n + 1 f’ = substitute f (Var x) (Fun ( skolemFunc n) mu) False n mu ( Quantifier Forall x f) = Quantifier Forall x (sk False n (mu ++ [Var x]) f)

36

sk True n mu ( Quantifier Exists x f) = Quantifier Exists x (sk True n (mu ++ [Var x]) f) sk False n mu ( Quantifier Exists x f) = sk False m mu f’ where m = n + 1 f’ = substitute f (Var x) (Fun ( skolemFunc n) mu)

37

Prover.hs module Prover ( allVariables , substituteTerm ,allRules ,applyRule , Formula (..) , Term (..) , Function ,Variable ,Predicate , Symbol (..) , Sequent ,fromFirst , setFirst , applyLeftRight ,substitute ,fnot ,for ,fand ,fimp ,fpred ,Proof (..) , LR (..) , Rule (..) , drinkerParadox ,proof)where import import import import

Formula Prelude hiding (Left , Right) Data.List Data.Maybe

proof :: Int -> Sequent -> Maybe Proof proof max s | len == Nothing | otherwise where len = proofLength max s

= Nothing = Just ( makeProof ( fromJust len) s)

makeProof :: Int -> Sequent -> Proof makeProof n s = c goodStep where goodStep :: RuleResult goodStep = head [t | t Proof c (rule , sequents ) = Proof rule s (map ( makeProof (n -1)) sequents ) proofLength :: Int -> Sequent -> Maybe Int proofLength max s | not ( hasProof max s) = Nothing | and [ hasProof max s,not ( hasProof (max -1) s)] = Just max | otherwise = proofLength (max - 1) s hasProofRule :: Int -> RuleResult -> Bool hasProofRule max (_ ,[]) = True hasProofRule max (_, sequents ) = and (map ( hasProof max) sequents ) hasProof :: Int -> Sequent -> Bool hasProof 0 _ = False hasProof max s = or (( map ( branchProvable (max -1))) branches ) where break :: (Rule ,[ Sequent ]) -> [ Sequent ] break (r,s) = s branches :: [[ Sequent ]] branches = map break ( applyLeftRight s) branchProvable :: Int -> [ Sequent ] -> Bool branchProvable _ [] = True branchProvable m sequents = and (map ( hasProof m) sequents ) applyRule :: Sequent -> Rule -> Maybe RuleResult applyRule s r | result == Nothing = Nothing | otherwise = Just (r, fromJust result ) where result = applyRule ’ s r applyRule ’ :: Sequent -> Rule -> Maybe [ Sequent ] applyRule ’ (( Unary Not a): gamma ,delta) ( SymbolRule Left Not) = Just [( gamma ,a:delta )] applyRule ’ (( Binary Or a b): gamma ,delta) ( SymbolRule Left Or) = Just [(a:gamma ,delta ),(b:gamma ,delta )] applyRule ’ (( Binary And a b): gamma ,delta) ( SymbolRule Left And) = Just [(a:b:gamma ,delta )] applyRule ’ (( Binary Imp a b): gamma ,delta) ( SymbolRule Left Imp)

38

= Just [( gamma ,a:delta ),(b:gamma ,delta )] applyRule ’ s@(( Quantifier Exists x a): gamma ,delta) ( QuantifierRule Left Exists t) | elem t ( termsS s) = Nothing | otherwise = Just [(a’: gamma ,delta )] where a’ = substitute a (Var x) t applyRule ’ (f@( Quantifier Forall x a): gamma ,delta) ( QuantifierRule Left Forall t) = Just [(a’:f:gamma ,delta )] where a’ = substitute a (Var x) t applyRule ’ (gamma ,delta) (Perm Left index) = Just [( setFirst index gamma ,delta )] applyRule ’ (gamma ,( Unary Not a): delta) ( SymbolRule Right Not) = Just [(a:gamma ,delta )] applyRule ’ (gamma ,( Binary Or a b): delta) ( SymbolRule Right Or) = Just [( gamma ,a:b:delta )] applyRule ’ (gamma ,( Binary And a b): delta) ( SymbolRule Right And) = Just [( gamma ,a:delta ),(gamma ,b:delta )] applyRule ’ (gamma ,( Binary Imp a b): delta) ( SymbolRule Right Imp) = Just [(a:gamma ,b:delta )] applyRule ’ (gamma ,f@( Quantifier Exists x a): delta) ( QuantifierRule Right Exists t) = Just [( gamma ,a’:f:delta )] where a’ = substitute a (Var x) t applyRule ’ s@(gamma ,( Quantifier Forall x a): delta) ( QuantifierRule Right Forall t) | elem t ( termsS s) = Nothing | otherwise = Just [( gamma ,a’: delta )] where a’ = substitute a (Var x) t applyRule ’ (gamma ,delta) (Perm Right index) = Just [( gamma , setFirst index delta )] applyRule ’ _ _ = Nothing applyLeftRight :: Sequent -> [ RuleResult ] applyLeftRight s@(ant ,suc) | and [ant /= [], suc /=[] , head ant == head suc] = [( Axiom ,[])] | otherwise = catMaybes $ map ( applyRule s) ( allRules s) allRules :: Sequent -> [Rule] allRules s@(gamma ,delta) = allSymbolRules ++ allPerms ++ allQuantifiers where allSymbolRules = [( SymbolRule lr symbol ) | lr [(Rule ,[ Sequent ])] permRight (gamma ,delta) = [( permRight ’ (gamma ,delta) i) | i Int -> (Rule ,[ Sequent ]) permRight ’ (gamma ,delta) index = (Perm Right index ,[( gamma , setFirst index delta )])

40

Main.hs module import import import import import

Main(main) where Functions Formula Expansion Data.Maybe Prover

f = Pred "p" [] f2 = Pred "q" [] f3 = Pred "r" [] f4 = Pred "s" [] skDrinker = skSequent ([] ,[ drinkerParadox ]) proofDrinker = fromJust (proof 10 $ skDrinker ) ([] , expDrinker :[]) = extract proofDrinker

expDeskDrinker = desk True 0 [] drinkerParadox expDrinker test = rmTF ([] ,[ drinkerParadox ]) (rm $ pr ([] ,[ expDeskDrinker ]))

main = do putStrLn $ show $ test

41