GAPT User Manual - Theory and Logic Group
Contents
1. y List Atom P s s 0 0 DAtom P s s s 0 0 0 s s 0 WeakQuantifier Vy P s s s 0 y DP s s s s 0 y List Atom P s s s 0 0 DAtom P s s s s 0 0 0 s s s 0 Atom P 0 0 WeakQuantifier Vx Vy P x y DP x s y List WeakQuantifier Vy P s s s s 0 y DP s s s s 0 8 y List C Atom P s s s s 0 0 DAtom P s s s s 0 8 0 0 Atom P s s s s 0 s 0 DAtom P s s s s 0 s s 0 8 0 Atom P s s s s This expansion sequent can then be viewed in the graphical user interface by simply calling gapt gt prooftool E A window then opens that displays the end sequent of p i e the shallow sequent of E You can then selectively expand quantifiers by clicking on them see 6 for a detailed description 4 10 Cut elimination by resolution CERES FiXme Short example for first and higher order CERES 4 11 Cut introduction The cut introduction algorithm as described in 5 4 3 is implemented in GAPT for introducing I4 cuts into a sequent calculus proof We will use as input one of the proofs generated by the system namely LinearExampleProof 9 But the user can also write his own proofs see Section 3 2 and input them to the cut introduction algorithm Take an example proof gapt gt val p LinearExampleProof 4 at logic gapt proofs lkNew LKProof 16 GAPT User Manual p18 Vx PG DP s x PCO P s s s s 02. 4 8 Interpolation The command ExtractInterpolant extracts an interpolant from a sequent calculus proof which may contain atomic cuts and or equality rules Currently we allow only reflexivity axioms and axioms of the form At A L H or T The implementation is based on Lemma 6 5 of 10 The method expects a proof p and an arbitrary partition of the end sequent I A of p into a negative part I y F Ay and a positive part T Ag It returns a formula J s t T4 F Ay Z and I T Ag are provable and J contains only such predicate symbols that appear in both T F Ay and I2 F Ag For instance suppose pr is the following proof First we construct the proof pr gapt gt val ca FOLConst a ca at logic gapt expr FO LConst gapt gt val cb FOLConst b cb at logic gapt expr FO LConst Pla F P a a b Pla lr Pla w 1 14 a b P a E P GAPT User Manual gapt gt val pa FOLAtom P List ca pa at logic gapt expr FOLAtom P a gapt gt val pb FOLAtom P List cb pb at logic gapt expr FOLAtom P b gapt gt val aeqb Eq ca cb aeqb at logic gapt expr FOLAtom a b gapt gt val axpa LogicalAxiom pa axpa at logic gapt proofs lkNew LogicalAxiom p1 PCa P a LogicalAxiom P a gapt gt val axpb LogicalAxiom pb axpb at logic gapt proofs lkNew LogicalAxiom p1 P b P b LogicalAxiom P b gapt gt val
3. A LogicalAxiom A To finish the proof it remains to apply two D right inferences gapt gt val p4 ImpRightRule p3 B F2 p4 at logic gapt proofs 1lkNew ImpRightRule p4 A BD AAB ImpRightRule p3 Ant 1 Suc 0 p3 A B AAB AndRightRule p1 Suc 0 p2 Suc 0 p2 B B LogicalAxiom B p1 A A LogicalAxiom A gapt gt val p5 ImpRightRule p4 A F1 po at logic gapt proofs 1lkNew ImpRightRule p5 AD BD AAB ImpRightRule p4 Ant 0 Suc 0 p4 A BDCAAB ImpRightRule p3 Ant 1 Suc 0 p3 A B AAB AndRightRule p1 Suc 0 p2 Suc 0 p2 B B LogicalAxiom B p1 A A LogicalAxiom A You can now view this proof by typing gapt gt prooftool p5 The system comes with a collection of example proof sequences in the file examples ProofSequences scala which are generated in the above style Have a look at this code for more complicated proof con structions 4 Feature walkthrough 4 1 SAT solver interface The following shows an example session using the Sat4j SAT solver to verify validity and satisfia bility and query the thus obtained models Consider the pigeon hole principle for m n PHP m n which states that if m pigeons are put into n holes then there is a hole which contains two pigeons It is valid iff m gt n PHP states that when putting m pigeons into n holes there is no hole containing two pigeons This is satisfiable
4. ForallLeftRule p14 Ant 0 PC b y DQ b y a y p14 P b a DQ b a dx dy Q y D P x y ContractionRightRule p13 Suc 0 Suc 1 p13 P b a DQ b a dx dy QG y D P x y dx dy Q x y D P x y ImpLeftRule p6 Suc 0 p12 Ant 0 p12 Q b a dx dy 4Q x y D P y ExistsRightRule p11 Suc 0 dy AQ x y D P x y b x p11 Q b a dy Q b y D P b y ExistsRightRule p10 Suc 0 Q b y D P b y a y p10 Q b a 7Q b a D P b a ImpRightRule p9 Ant 0 Suc 0 p9 Q b a Q b a P b a WeakeningRightRul 4 7 Skolemization Skolemization consists of replacing the variables bound by strong quantifiers in the end sequent of a proof by new function symbols thus obtaining a validity equivalent sequent In the GAPT system Skolemization is implemented for proofs and can be used e g as follows gapt gt val Seq x y Seq x y map FOLVar _ x at logic gapt expr FOLVar x y at logic gapt expr FOLVar y gapt gt val Pxy FOLAtom P x y Pxy at logic gapt expr FOLAtom P x y gapt gt var p LKProof LogicalAxiom Pxy p at logic gapt proofs lkNew LKProof p1 P x y P x y LogicalAxiom P x y gapt gt p ExistsRightRule p Ex x Pxy x p at logic gapt proofs 1kNew LKProof p2 P x y 3x P x y ExistsRightRule p1 Suc 0 P x y x x p1 P x y P x y LogicalAxiom P x y gapt gt p ForallLe
5. GAPT General Architecture for Proof Theory User manual Version 1 11 SNAPSHOT December 15 2015 GAPT User Manual List of Corrections Contents 1 Introduction 2 Download and execution 2 1 System requirements 2 2 3 Data structures 31 Formulas oioorisrrsdrs or rs ehe eb an Be II a Be et ed 4 Feature walkthrough 4 1 SAT solver interface o ce dorre ioi on ian a a e 4 2 MaxSAT solver interface e 4 3 SMT solver interface oaoa a 4 4 First order theorem prover interface o 0 00 ee 4 5 Built in tableaux prover o e see we eda o 4 6 Cut elimination Gentzen s method 00 000 e e AT Skolemization ee s esege i kee a aaa a ee 48 interpolation i 244405548 G Se a See SEG ee RE EE SS 4 9 Expansion trees 2 5 sei eo 4 eR ee era e RR eee 4 10 Cut elimination by resolution CERES ooo o AL CURIPATOGUGHON 2 2 2 45 4 2 oe eal gee bb Be eee Re we Ace S 4 12 Teo EINA ocio he Oe oe he ee ee ee eee ets A Proof systems AU es ee E ee Se oe Ad Se ee a ee al oO on OQ 12 12 13 14 15 16 16 18 GAPT User Manual B Prover9 term parser parseFormula 26 B 1 LADR naming scheme default ee 26 B 2 Prolog naming scheme 0000 ee a 26 B 3 Terms and Formulas 2 aats ioatea naa a a aaa a a e a aa a a 27 C XML proof parser 27 GAPT User Manual 1 Introduction GAPT is a generic architecture for pro
6. Boolean true 4 2 MaxSAT solver interface The MaxSAT interface supports generating optimal solutions for weighted partial MaxSAT instances these consist of a list of hard clauses which must be satisfied in the solution and a list of weighted soft clauses where weight of the satisfied soft clauses must be maximized See 1 for an overview Let us solve a simple example using the MaxSAT solver from SAT4J gapt gt val Seq a b c Seq a b c map FOLAtom _ a at logic gapt expr FOLAtom a b at logic gapt expr FOLAtom b c at logic gapt expr FOLAtom c gapt gt MaxSat4j solve hard alblc soft Seq a gt 4 b gt 3 GAPT User Manual resi3 Option at logic gapt models Interpretation Some a gt false b gt false c gt true GAPT also supports other MaxSAT solvers out of the box just write OpenWBO or ToySolver instead of MaxSat4j 4 3 SMT solver interface The SMT solver interface in GAPT supports validity queries for QF_UF formulas For example we can check whether a quantifier free formula is a quasi tautology using veriT gapt gt val f parseFormula a b a c P c P b gt P a f at logic gapt expr FOLFormula a bVa c A P c AP b DP a gapt gt VeriT isValid f res14 Boolean true GAPT also supports Z3 and CVC4 out of the box if they are installed gapt gt Z3 isValid f resi5 Boolean true gapt gt CVC4 isValid f res16 Boolean true Yo
7. BussTautology 5 f at logic gapt proofs HOLSequent c_1Vd_1 A c_2Vd_2 A c_3Vd_3 A c_4Vd_4 yDce_5IVCCCC c_1Vd_1 A c_2Vd_2 A c_3Vd_3 A c_4Vd_4 Dd_5 CC c_1Vd_1 AC c_2Vd_2 A c_38Vd_3 Dc_4 VC c_1Vd_1 ACc_2Vd_2 A c_3Vd_3 Dd_4 c_1V d_1 A c_2Vd_2 Dce_3 VCC c_1Vd_1 A c_2Vd_2 Dd_3 c_1Vd_1 gt c0_2 V c_1Vd_1 Dd_2 c_1Vd_1 c5 d5 3 2 Proofs There are various possibilities for entering proofs into the system The most basic one is a direct top down proof construction using the constructors of the inference rules gapt gt val A FOLAtom A A at logic gapt expr FOLAtom A gapt gt val B FOLAtom B B at logic gapt expr FOLAtom B gapt gt val Fi B gt A amp B F1 at logic gapt expr FOLFormula BD AAB gapt gt val F2 A amp B F2 at logic gapt expr FOLFormula AMB We start with the axioms gapt gt val pi LogicalAxiom A pl at logic gapt proofs lkNew LogicalAxiom p1 A A LogicalAxiom A gapt gt val p2 LogicalAxiom B p2 at logic gapt proofs lkNew LogicalAxiom p1 B B LogicalAxiom B These are joined by an A right inference See Appendix A 1 for the formal definition of the sequent calculus used in GAPT GAPT User Manual gapt gt val p3 AndRightRule pi A p2 B p3 at logic gapt proofs 1kNew AndRightRule p3 A B AAB AndRightRule p1 Suc 0 p2 Suc 0 p2 B B LogicalAxiom B p1 A
8. ContractionLeftRule p17 Ant 0 Ant 2 p17 Vx PG DP s x PCO Vx P x DP s x P s s s s 0 ForallLeftRule p16 Ant 0 P x DP s x 0 x p16 P 0 DP s 0 P 0 Vx P x DP s x P s s s s 0 ImpLeftRule p1 Suc 0 p15 Ant 1 p15 Vx PG DP s P s 0 P s s s s 0 ContractionLeftRule p14 Ant 0 Ant 2 p14 Vx P x DP s x P s 0 Vx P x DP s x P s s s s 0 ForallLeftRule p13 Ant 0 P x D gt P s x sO x p13 P s 0 DP s s 0 P s 0 Vx P x DP s x P s s s s 0 ImpLeftRule p2 Suc 0 p12 Ant 1 p12 Vx P x DP s x P s s 0 P s s s s 0 ContractionLeftRule p11 Then compute a proof with a single cut that contains a single quantifier by gapt gt val q CutIntroduction compressLKProof p DeltaTableMethod manyQuantifiers false verbose true Total inferences in the input proof 16 Quantifier inferences in the input proof 4 End sequent Vx P x DP s x P O P s s s s 0 Size of term set 6 Smallest grammar of size 6 Axiom T Non terminal vectors T a_0 Productions 7 gt P 0 _al T gt Vx P x DP s x _a0 s a_0 T gt Vx P x DP s x _a0 Ca_0 T gt P s s s s 0 _s0 a_0 gt 0 a_0 gt s s 0 Size of the canonical solution 8 Size of the minimized solution 4 CNF of minimized cut formula number 0 P a_0 P s s a_
9. SkolemQuantifier Vy 3x P x y s_ 2 WeakQuantifier J x P x s_ 2 List Atom P s_ 0 s_ 2 s_ 0 11 GAPT User Manual The LeanCoP interface only supports the getExpansionSequent method with exactly one formula in the succedent gapt gt LeanCoP getExpansionSequent sequent map toDeep _ res24 Option at logic gapt proofs HOLSequent Some p 0 p O Dp s 0 AC s 0 Dp s s 0 pls s 0 You can also export sequents in TPTP format if you want to pass them to other provers manually gapt gt TPTPFOLExporter tptp_proof_problem_split sequent res25 String fof formula0 axiom p 0 fof formulal axiom XO p X0 gt p s X0 fof formula2 conjecture p s s 0 4 5 Built in tableaux prover GAPT contains a built in tableaux prover for propositional logic which can be called with the command solve solvePropositional for example as in gapt gt solve solvePropositional parseFormula a gt b gt agb res26 Option at logic gapt proofs 1kNew LKProof Some p5 aDd bD aAb ImpRightRule p4 Ant 0 Suc 0 p4 a bD aAb ImpRightRule p3 Ant 1 Suc 0 p3 a b aAb AndRightRule p1 Suc 0 p2 Suc 0 p2 b b LogicalAxiom b pil a a LogicalAxiom a 4 6 Cut elimination Gentzen s method The GAP T system contains an implementation of reductive cut elimina
10. Wx Wy P x y0 x y 3x 3Jy 70 x y DP x y CutRule p13 Suc 0 p24 Ant 0 p24 Vx J3y HP x y VWQ x y 3x JIy H0 x y 5 P x y ForallLeftRule p23 Ant 0 dy 4P x y VQ x y b x p23 Sy AFP VQ b y dx dy Q x y D P x y ExistsLeftRule p22 Ant 0 v y p22 P b v VQ b v 3x Jy Q x y D P x y ExistsRightRule p21 Suc 0 dy Q x y DAP x y b x p21 P b v VQ b v dy 4Q b y D P b y ExistsRightRule p20 Suc 0 Q b y gt P b y v y p20 P b v VQ b v 4Q b v D P b v ImpRightRule p19 Ant 1 Suc 0 p19 P b v VQ b v Q b v aP b v OrLeftRule p16 Ant 0 p18 Ant 1 p18 Q b v Q b v NegLeftRule p17 Suc 0 p17 QC You can then view this proof in the graphical user interface prooftool by entering gapt gt prooftool proof In the folder examples simple you can find a number of further simple proofs 28 GAPT User Manual References 1 Josep Argelich Chu Min Li Felip Manya and Jordi Planes The first and second max SAT evaluations Journal on Satisfiability Boolean Modeling and Computation 4 2 4 251 278 2008 2 Matthias Baaz and Alexander Leitsch Cut elimination and Redundancy elimination by Reso lution Journal of Symbolic Computation 29 2 149 176 2000 3 Stefan Hetzl Alexander Leitsch Giselle Reis Janos Tapolczai and Daniel Weller Introducing Quantified Cuts in Logic
11. logic gapt proofs 1kNew LKProof Some p191 p 0 Vx p x Dp s x p s s 0 CutRule p3 Suc 0 p18 Ant 1 p18 Vx p x Dp s x pO p s s 0 ContractionLeftRule p17 Ant 2 Ant 0 p17 Vx p x Dp s x pCO Vx p x Dp s x p s s 0 CutRule p8 Suc 0 p16 Ant 1 p16 Vx p x Dp s x p s 0 p s s 0 CutRule p13 Suc 0 p15 Ant 0 p15 p s s O p s s 0 ContractionRightRule p14 Suc 0 Suc 1 p14 p s s 0 p s s 0 p s s 0 WeakeningRightRule p9 p s s 0 p13 Vx p x Dp s x p s 0 p s s 0 ContractionLeftRule p12 Ant 0 Ant 1 p12 Vx p x Dp sG Vx x Dp s x p s 0 p s s 0 WeakeningLeftRule p11 Vx pG Dp s x p11 Vx p x Note that getLKProof only works for sequents without strong quantifiers i e sequents that are already Skolemized however getExpansionSequent will happily return expansion sequents with Skolem quantifiers in that case gapt gt val strong exists x all y P x y Sequent all y exists x P x y map parseFormula strong at logic gapt proofs Sequent at logic gapt expr FOLFormula Jx Vy P x y Vy dx P x y gapt gt Prover9 getExpansionSequent strong res23 Option at logic gapt proofs expansionTrees ExpansionSequent Some SkolemQuantifier dx Vy P x y s_ 0 WeakQuantifier Vy P s_ O y List Atom P s_ 0 s_ 2 s_ 2
12. proof WeakeningLeftRule axpa aeqb proof at logic gapt proofs 1lkNew WeakeningLeftRule p2 a b P a P a WeakeningleftRule p1 a b p1 PCa P a LogicalAxiom P a gapt gt val pr EqualityRightRule proof aeqb Suc O pb pr at logic gapt proofs lkNew EqualityRightRule p3 a b P a P b EqualityRightRule p2 Ant 0 Suc 0 2 p2 a b P a P a WeakeningleftRule p1 a b p1 P a P a LogicalAxiom P a In order to apply interpolation we need to specify a partition of the end sequent into I F Aj and T2 F Ag i e into the negative npart and positive ppart part respectively In this case we set Ai P b T2 a b P a and Ty Ag Then we can call ExtractInterpolant pr npart ppart which returns the interpolant I a b D P a of pr gapt gt val I ExtractInterpolant pr Seq Suc 0 Seq Ant O Ant 1 I at logic gapt expr HOLFormula a bD P a 4 9 Expansion trees Expansion trees are a compact representation of cut free proofs They have originally been intro duced in 8 GAPT contains an implementation of expansion trees for higher order logic including functions for extracting expansion trees from proofs for merging expansion trees for pruning and transforming them in various ways and for viewing them in a comfortable way in the graphical user interface An expansion tree contains the instances of the quantifiers for a f
13. 0 Number of cuts introduced 1 Total inferences in the proof with cut s 19 Quantifier inferences in the proof with cut s 5 q Option at logic gapt proofs 1kNew LKProof Some p19 Vx P x DP s x PQ P s s s s CutRule p10 Suc 0 p18 Ant 17 GAPT User Manual 0 p18 Va_0 P a_0 gt P s s a_0 P O P s s s s 0 ContractionLeftRule p17 Ant 1 Ant 0 p17 Va_0 P a_0 gt P s s a_0 Va_0 P a_0 gt P s s a_0 PQ P s s s s O ForallLeftRule p16 Ant 2 P a _0 DP s s a_0 s s 0 a_0 p16 Va_0 P a_0 D gt P s s a _0 PCO P s s 0 DP s s s s 0 P s s s s 0 ForallLeftRule p15 Ant 0 P a_0 gt P s s a_0 0 a_0 p15 P 0 D gt P s s 0 PCO P s s 0 DP s s s s 0 P s s s s 0 ImpLeftRule p11 Suc 0 p14 Ant 1 p14 P s s 0 DP s s s s 0 P s s 0 P s s s s 0 ImpLeftRule p12 Suc 0 p13 Ant 0 p13 You can also try DeltaTableMethod manyQuantifiers true this will proceed as above but will compute a single cut with a block of quantifiers The method MaxSATMethod 1 2 uses a reduction to a MaxSAT problem and an external MaxSAT solver for finding a minimal grammar corresponding to a proof with a cut with two cuts one with 1 quantifier one with 2 quantifiers 4 12 Tree grammars The cut introduction method described in Section 4 11 is based on the use of certain tree gramma
14. CELANTE TEA A BYTA A T H A B FiXme Expansion trees B Prover9 term parser parseFormula The Prover9 parser interprets names strings built over the alphabet a z A Z 0 9 Also the equality symbol and the arithmetic operators are names Since prover 9 has two naming schemes we describe both of them The default is the native LADR scheme B 1 LADR naming scheme default Names starting with lower case letters from u to z are interpreted as variable symbols Every name starting with a different letter is interpreted as a constant function predicate symbol depending on the position in the term B 2 Prolog naming scheme Names starting with upper case letters from A to Z are interpreted as variable symbols Every name starting with a different letter is interpreted as a constant function depending on the position in the term Predicates start with a lower or an upper case letter 26 FiXme GAPT User Manual B 3 Terms and Formulas Arguments are always separated by commas and put in parenthesis Terms are built from variable constant symbols and function symbols applied to a number of arguments which are terms Like wise atoms are predicate symbols possibly with arguments which are again terms The function symbols and the equality predicate are written in infix notation For example the following are terms in the LADR naming scheme constant variable function
15. _3 R p_1 h_3 R p_3 h_3 R p_2 h_3 2 37 R p_2 h_1 R p_2 h_2 R p_2 h_3 R p_3 h_3 R p_1 h_3 R p_2 h_1 R p_1 h_1 R p_3 h_2 R p_1 h_2 R p_3 h_1 R p_1 h_1 R p_3 h_1 R p_2 h_1 R p_2 h_2 R p_1 h_2 R p_1 h_1 R p_1 h_2 RC p_1 h_3 gapt gt val encoding new DIMACSEncoding encoding at logic gapt formats dimacs DIMACSEncoding DIMACSEncoding gapt gt writeDIMACS encoding encodeCNF cnf res8 String p cnf 9 12 1230 2 4 0 GAPT User Manual Lbs OSSD ol ON Ww Wo bo ke NDONWUDADANDAD pi j i l O OOGO O O O O OO 00 co If you want to know which variable in the DIMACS output corresponds to which atom in GAPT you can query the DIMACSEncoding object gapt gt encoding decodeAtom 1 res9 at logic gapt expr HOLAtom R p_3 h_1 GAPT also supports other SAT solvers such as MiniSAT or Glucose out of the box gapt gt MiniSAT isValid PigeonHolePrinciple 3 2 res10 Boolean true gapt gt Glucose isValid PigeonHolePrinciple 3 2 res11 Boolean true If you have another DIMACS compliant solver installed or want to pass extra options to the SAT solver you can pass a custom command to GAPT as well gapt gt val solver new ExternalSATSolver minisat mem lim 1024 solver at logic gapt provers sat ExternalSATSolver ExternalSATSolver minisat mem 1im 1024 gapt gt solver isValid PigeonHolePrinciple 3 2 res12
16. a library in your Scala project it is available as a Maven artifact on JCenter All you need to do is add one line to your build sbt libraryDependencies at logic gapt gapt 1 10 The command line interface of GAPT is an interactive Scala shell This means that all functionality of Scala is available to you In particular it is easy to write Scala scripts that use the functionality of GAPT You don t need to know anything about Scala to try out the examples in this manual but if you do want to learn more about Scala we recommend the book Programming in Scala 9 Interactions with the Scala shell are typeset in the following way GAPT User Manual gapt gt println Hello world Hello world Here println Hello world is the user input and Hello world is the output from the Scala shell If you want to consult the in depth API documentation of a function you can use the help command gapt gt help containsQuantifierOnLogicalLevel 2 1 System requirements To run GAPT you need to have Java 7 or higher installed GAPT contains interfaces to the following automated reasoning systems Installing them is optional If GAPT does not find the executables in the path the functionality of these systems will not be available e Prover9 http www cs unm edu mccune mace4 download make sure the commands prover9 and prooftrans are available e E theorem prover http eprover org e LeanC
17. constant variable s 21 5 And the following are atoms P1 alpha beta x 25 v The logical connectives are called amp gt all exists where the quantifiers and negation are written in prefix form and conjunction disjunction and implication are written in infix form Conjunction and disjunction are right associative Quantifiers always need to be enclosed in paren thesis but a series of quantifiers doesn t need parenthesis in between The binding order is from strongest to weakest Y 3 AV gt For example the formula Vx P x f x gt 3yP x y is parsed as gapt gt parseFormula all x P x f x gt exists y P x y res30 at logic gapt expr FOLFormula Vx P x f x Ddy P x y The Prolog scheme can be parsed as well using the Prover9TermParser class gapt gt Prover9TermParser parseFormula all X P X f X gt exists Y P X Y res31 at logic gapt expr FOLFormula VX P X f X DdY P X Y C XML proof parser This method XMLProofDatabaseParser will take as an argument a string that represents the path of a file containing a proof database in the XML format generated by HLK for example and will return a proof database containing a list of pairs It expects a file the string of a proof will not work and you can use the relative path In the list returned each pair is composed of a string and an object representing a proof within the system The string is the
18. ftRule p All y Pxy y p at logic gapt proofs lkNew LKProof p3 Vy P x y dx P x y ForallLeftRule p2 Ant 0 P x y y y p2 P x y dx P x y ExistsRightRule p1 Suc 0 P x y x x 13 GAPT User Manual p1 P x y P x y LogicalAxiom P x y gapt gt p ForallRightRule p All y Ex x Pxy y p at logic gapt proofs lkNew LKProof p4 Vy P x y s yya P x y C ForallRightRule p3 Suc 0 y y p3 Vy P x y dx P x y ForallLeftRule p2 Ant 0 P x y y y p2 P x y dx P x y ExistsRightRule p1 Suc 0 P x y x x p1 P x y P x y LogicalAxiom P x y gapt gt p ExistsLeftRule p Ex x All y Pxy x p at logic gapt proofs lkNew LKProof ExistsLeftRule p4 Ant 0 x x p5 3 x Vy P x y 2 y 20 PG y p4 Vy P x y Vy dx P x y ForallRightRule p3 Suc 0 y y p3 Vy P x y 3x P x y ForallLeftRule p2 Ant 0 P x y y y p2 P x y 3x P x y p1 P x y P x y LogicalAxiom P x y gapt gt val q skolemize p q at logic gapt proofs lkNew LKProof ExistsRightRule p1 Suc 0 P x y x x p3 Vy P s_ 0 y 3x P x s_ 1 ForallLeftRule p2 Ant 0 P s_10 y s_ 1 y p2 P s_ 0 s_ 1 dx P x s_ 1 x ExistsRightRule p1 Suc 0 P x s_ 1 s_ 0 p1 P s_ 0 s_ 1 P s_ 0 s_ 1 LogicalAxiom P s_ 0 s_ 1
19. he constructors of a type and let k be the arity of ci Let Flx be a formula with x a free variable of the appropriate type Then we call the sequent S Flzx1 Flxz D Ai Fles x1 ux the i th induction step In this case the induction rule has the form m m Tn Si Sa es TKA V2F a Sn ind In the case of the natural numbers there are two constructors 0 of arity O and s of arity 1 Consequently the induction rule reduces to m1 r F Ay F 0 F z T2 F As Flsz 112 ind T P gt f Ay Ag Yz F a A 2 Resolution Initial clauses ron InputClause TER ReflexivityClause Ey Sa TautologyClause Structural rules aVaVC avC Factor C Instance Co 22 GAPT User Manual Logical rules CVa YD Resolution CVD CVt s lt v D Cvlls v D Paramodulation CVi 8 l s v D Cv It VD Paramodulation A 3 LKsk LKsk is a sequent calculus used in the CERES method for higher order logic see 11 for an overview of both the calculus and the method LKsk operates on labelled formulas A label is a finite list of terms a labelled formula is a pair F 2 written as F If Lis a label and t a term we write t for the concatenation of and t Axioms AA Aye Logical axiom Paap Reflexivity axiom ye E axiom 7 Theory axiom AN S e Ayer F BD PESI Bn Logical axioms and theory axioms may only conta
20. iff m lt n gapt gt Sat4j isValid PigeonHolePrinciple 3 2 res3 Boolean true shows that PHP3 2 is valid and gapt gt Sat4j isValid PigeonHolePrinciple 3 3 res4 Boolean false ln Scala Sat4j isValid formula is syntactic sugar for Sat4j isValid formula GAPT User Manual shows that PHP3 3 is not valid Furthermore gapt gt val Some m Sat4j solve PigeonHolePrinciple 3 3 m at logic gapt models Interpretation R p_1 h_1 gt false R p_1 h_2 gt false R p_1 h_3 gt true R p_2 h_1 gt true R p_2 h_2 gt false R p_2 h_3 gt false R p_3 h_1 gt false R p_3 h_2 gt true R p_3 h_3 gt false yields a model of PHP33 that can be queried gapt gt val pi PigeonHolePrinciple atom 1 1 pl at logic gapt expr FOLAtom R p_1 h_1 gapt gt val p2 PigeonHolePrinciple atom 2 1 p2 at logic gapt expr FOLAtom R p_2 h_1 gapt gt m interpret p1 Is pigeon 1 in hole 1 res5 Boolean false gapt gt m interpret p2 Is pigeon 2 in hole 1 res6 Boolean true We can also interpret quantifier free formulas gapt gt m interpret And p1 p2 res7 Boolean false We can also convert PHP33 into DIMACS format gapt gt val cnf _ _ structuralCNF PigeonHolePrinciple 3 3 generateJustifications false propositional true cnf Setlat logic gapt proofs HOLClause Set R p_3 h_1 R p_3 h_2 R p_3 h_3 R p_3 h_2 R p_2 h_2 R p_2 h
21. igher order logic 2010 Wien Techn Univ Diss 2010 29
22. in atomic formulas Cut PRA 4 SEI TEFA N i Note that the labels of the cut formulas do not need to be equal Structural rules Left rules AR Ay TEFA ALTEA c l TEA ara M 23 GAPT User Manual Right rules TEA Wed THA A gt Propositional rules Left rules A BY TEA An BY TFA A I AY TEA BY E FI AWB T amp F Asi v 1 PPARA 7 AA TRA gt THA AE BY EFI A gt By se eat O Quantifier rules Left rules A t x 6t TRA WAY TRA v 1 Aly a PEA JA TEA 3 1 A f Q a TF A HAT H A 3 1 Right rules DEALS SPB T EFA ML AA BY A r PEA Ay BY TFA Av By Vir ALTEA oe O A TE A BY THA AD By O r Right rules PEA Aly a TEA VrA V r TEA ALO 2 Uk TEA VIA l TEA Alt z a TEA arAy The variable y must not occur free in T A or A The term t must avoid variable capture i e it must not contain free occurrences of variables bound in A Equality rules 24 GAPT User Manual Left rules Right rules s t A T s ain s E FIL Als ye a s 04 A T 2 5 H 4 5FU AITA s A T t 4 E II 4 s H E FH I A T t ep s 294 arpa en s 9 5F1 A T s Each equation rule replaces exactly one occurrence of a term in its auxiliary for
23. mula A 4 Ral Ral is a higher order resolution calculus used in the CERES method for higher order logic see again 11 for details Ral operates on sequents of labelled formulas just as LKsk A label is a finite set of terms a labelled formula is a pair F written as F If is a label and a term we write t for the concatenation of and t TEA Rallnitial The substitution also substitutes the variables in the labels TEA To F Ag RalSub The resolution rule does not require the labels to be equal TRA WA Ayo AVS A SHI LEAN RalCut Factoring is restricted to atoms a a a THA TEA a a 7 RalFactor 7 ot TFA TRA RalFactor Paramodulation can rewrite the equation in both directions in a formula of the antecedent or the succedent this is one of the four possibilities THA t s HI Aft T EF A Als y RalPara 25 GAPT User Manual Va Ale PRA TE A vz Ala 7 RalAllF 7 7 RalAllT AS TFA T F A Ala 60 dx Ale T FA TH A de Alz 7 RalExF 7 RalExT Ala T FA TEA A s TY TFA reA 1 A RalTopF TEA gt RalBottomT SAY TEA TEA 4 AA RalNegF AGA RalNegT TEA A ALTEA An B TEHA nindi THA AABY Saai THA AMB Anati A BY TFA O TRA Ae m TRA Be Vem AVBYTEA Ei AV BY TEA ee THA AV By a Alten 709 BY THKA S TEA A Bye ot ASBFTEA AD BETA TRA AS BY woes Raline AAA RallmpF2
24. name of the proof defined in the XML file For example gapt gt val proofs XMLProofDatabaseParser examples simple fol1 xml gz proofs proofs List String at logic gapt proofs 1kNew LKProof List p p25 Vx Vy P x y DQ x y dx dy 40 x y D P x y CutRule p13 Suc 0 p24 Ant 0 p24 Vx dy P x y VQ x y dx dy 50 x y gt P x y ForallLeftRule p23 Ant 0 dy P x y VQx y b x p23 dy P b y VQ b y dx dy Q x y DAP x y ExistsLeftRule p22 Ant 0 v gt y p22 P b v VQ b v 3x Jy Q x y D P x y ExistsRightRule p21 Suc 0 Jy C90 x y DAP x y b x 27 GAPT User Manual p21 P b v VQ b v Jy H0Q b y D P b y ExistsRightRule p20 Suc 0 00 y D gt P b y v y p20 P b v VQ b v Q b v D P b v ImpRightRule p19 Ant 1 Suc 0 p19 P b v VQ b v gt Q b v P b v OrLeftRule p16 Ant 0 p18 Ant 1 p18 Q b v Q b v NegLeftRul returns a list of length 1 as shown by entering gapt gt proofs length res32 Int 1 Its only element is proofs 0 the name of this proof can be obtained by entering gapt gt proofs 0 _1 res33 String p and the proof itself by gapt gt val proof proofs 0 _2 proof at logic gapt proofs lkNew LKProof p25
25. oP http leancop de e VeriT http www verit solver org e Z3 https github com Z3Prover z3 e MiniSAT http minisat se e Glucose http www labri fr perso 1simon glucose e Sat4J http sat4j org e OpenWBO http sat inesc id pt open wbo e CVC4 http cvc4 cs nyu edu web 3 Data structures 3 1 Formulas Formulas terms and other expressions are are represented as lambda terms in simple type theory Terms and formulas of first order logic and schematic first order logic are hence encoded as lambda terms these form regular subsets You can enter formulas by parsing them with the prover9 7 parser GAPT User Manual gapt gt val H parseFormula all x P x f x gt exists y P x y H at logic gapt expr FOLFormula Vx P x f x Ddy P x y The prover9 syntax was also extended to higher order logic where type declarations are added gapt gt val I parseLLKFormula var P 0 gt i gt o const f o gt i var x 0 var y i all x P x f x gt exists y P x y I at logic gapt expr HOLFormula Vx o P x f x Ddy P x y Please refer to Appendix B for a full description of the languages the parsers accept A collection of formula sequences can be found in the file examples FormulaSequences scala Have a look at this code to see how to compose formulas without the parser You can generate instances of these formula sequences by entering e g gapt gt val f
26. of transformations implemented in Scala The focus of GAPT are proof transformations in contrast to proof assistants whose focus is proof formalization and automated deduction systems whose focus is proof search GAPT is used from a shell that provides access to the functionality in the system in a way that is inspired by computer algebra systems the basic objects are formulas and different kinds of proofs which can be modified by calling GAPT commands from the command line In addition there is a graphical user interface that allows the user to view and to a certain extent modify proofs in a flexible and visually appealing way The current functionality of GAPT includes data structures for formulas sequents resolution proofs sequent calculus proofs expansion tree proofs and algorithms for e g unification proof Skolemiza tion cut elimination cut elimination by resolution 2 cut introduction 5 etc 2 Download and execution There are three ways you can obtain GAPT 1 The recommended way You can download a package of the current version of GAPT at https logic at gapt After extracting the tar gz file you will find a shell script gapt sh Running this script will start the command line interface of GAPT gapt sh 2 If you are adventurous you can also download an unstable development version from github git clone https github com gapt gapt cd gapt sbt console 3 If you like GAPT and want to use it as
27. om P b DAtom P a a b Atom a b VAtom a c AAtom P c AAtom P b DAtom P a gapt gt extractInstances expansionSequent foreach println a bDb a a cDc a c aAP c DP a b aAP b DP a a bVa c A P c AP b DP a 4 4 First order theorem prover interface GAPT includes interfaces to several first order theorem provers such as Prover9 E prover and LeanCoP For Prover9 and E prover we can read back resolution proofs and construct LK and expansion proofs from them The LeanCoP interface only supports expansion sequent extraction Here is how you can get all of these kinds of proofs using Prover9 gapt gt val sequent existsclosure p 0 p x gt p s x Sequent p s s 0 map parseFormula sequent at logic gapt proofs HOLSequent p 0 Vx p x Dp s x p s s 0 gapt gt Prover9 isValid sequent res18 Boolean true gapt gt Prover9 getRobinsonProof sequent resi9 Option at logic gapt proofs resolution ResolutionProof Some p11 Resolution p6 Suc 0 p10 Ant 0 p10 p s 0 Resolution p7 Suc 0 p9 Ant 0 p9 p s s 0 Instance p8 Substitution p8 p s s 0 InputClause p s s 0 p7 p s 0 p s s 0 Instance p4 Substitution v0 gt s 0 p6 p s 0 Resolution p2 Suc 0 p5 Ant 0 p5 p 0 p s 0 Instance p4 Substitution v0 gt 0 p4 p vo p s v0 Instance p3 Substituti
28. on x gt v0 p3 p x p s x InputClause p x p s x p2 p 0 Instance p1 Substitution p1 p 0 InputClause p 0 gapt gt Prover9 getLKProof sequent res20 Option at logic gapt proofs 1kNew LKProof 10 GAPT User Manual Some p19 Vx p x Dp s x pCO p s s O ContractionLeftRule p18 Ant 2 Ant 1 p18 pCO Vx p x Dp s x Vx p x Dp s x p s s 0 CutRule p9 Suc 0 p17 Ant 1 p17 Vx pG Dp s p s 0 p s s 0 CutRule p14 Suc 0 p16 Ant 0 p16 p s s O pls s O ContractionRightRule p15 Suc 0 Suc 1 p15 p s s 0 p s s 0 p s s 0 WeakeningRightRule p10 p s s 0 p14 Vx p x Dp s x p s 0 p s s 0 ContractionLeftRule p13 Ant 0 Ant 1 p13 Vx p x Dp sG Vx x Dp s x p s 0 p s s 0 WeakeningLeftRule p12 Vx pG Dp s x p12 Vx p x Dp sG p s 0 p s s 0 ForallLeftRule p11 Ant 0 p x Dp SCFI saa gapt gt Prover9 getExpansionSequent sequent res21 Optionlat logic gapt proofs expansionTrees ExpansionSequent Some Atom p 0 WeakQuantifier Vx p x Dp s x List Atom p 0 DAtom p s 0 0 Atom p s 0 DAtom p s s 0 8 0 Atom p s s 0 All of the above works with E prover as well we will just show getLKProof as an example gapt gt EProver getLKProof sequent res22 Option at
29. ormula In order to represent an LK proof we use expansion sequents i e sequents of expansion trees We can obtain an expansion sequent for example by 15 GAPT User Manual gapt gt val p SquareEdgesExampleProof 4 p p40 Vx Vy P x y DP s x y P 0 0 Vx Vy P x y DP x s y P s s s s 0 at logic gapt proofs lkNew LKProof s s s s 0 ContractionLeftRule p39 Ant 0 Ant 2 p39 Vx Vy Px y DP s x y PC 0 0 Vx Vy P x y DP s x y Vx Vy P x y gt P x s y P s s s s 0 s s s s 0 ForallLeftRule p38 Ant 0 Vy P x y DP s x y 0 x p38 Vy P y DP s 0 y P 0 0 Vx Vy P x y DP s x y Vx Vy P x y DP x s y P s s s s 0 s s s s 0 ForallLeftRule p37 Ant 0 P 0 y DP s 0 y 0 y p37 P 0 0 D gt P s 0 0 PC 0 0 Vx Vy P x y DP sG y Vx Vy P x y P x s y P s s s s 0 s s s s 0 ImpLeftRule p1 Suc 0 p36 Ant 1 p36 Vx Vy Px y DP s x y P s 0 0 Vx Vy P x y P x s y P s s s s 0 gapt gt val E LKToExpansionProof p p at logic gapt proofs expansionTrees ExpansionSequent WeakQuantifier Vx Vy P x y DP s x y List WeakQuantifier Vy P 0 y DP s 0 y List Atom P 0 0 D Atom P s 0 0 0 0 WeakQuantifier Vy P s 0 y DP s s 0 y List Atom P s 0 0 DAtom P s s 0 0 0 s 0 CWeakQuantifier Vy P s s 0 y DP s s s 0
30. rs for representing Herbrand disjunctions These are totally rigid acyclic tree grammars TRATGs and vectorial TRATGs VTRATGs As shown in 4 these grammars are intimately related to the structure of proofs with cuts GAPT contains an implementation of these tree grammars and given a finite tree language i e a set of terms is able to automatically find a V TRATG that covers this language gapt gt val lang 1 to 18 map Numeral _ lang scala collection immutable IndexedSeq at logic gapt expr FOLTerm Vector s 0 s s O s s s 0 s s s s 0 s s s s s 0 sCs s s s s 0 s s s s s s s 0 s s s s s s s s 0 sCs s s s s s s s00 s s s s s s s s s s 0 sGs s s s s s s s s s 0 sCs s s ss s 8 s s s s 0 s s s s s s s s s s s s s 0 s s s s s s s s s s s s s s 0 s s s s s s s s s s s s s s s 0 D s s s s s s s s s s s s s s s s 0 s s s s s s s s s s s s s s s s s 0 s s s s s s s s s s s s s s s s s s 0 n gapt gt val grammar findMinimalGrammar lang 2 grammar at logic gapt grammars TratGrammar Axiom T Non terminals 7 a_1 a_2 Productions T gt s s s s a_1 T gt s a_1 a_i gt s s a_2 a_i gt s a_2 a_1 gt a_2 a_2 gt 0 18 GAPT User Manual a_2 gt s s s s s s 0 a_2 gt s s s s s s
31. s s s s s s 0 gapt gt lang toSet subsetOf grammar language res28 Boolean true You can also find minimal sub grammars that still generate certain terms gapt gt minimizeGrammar grammar Set 1 2 4 5 map Numeral _ res29 at logic gapt grammars TratGrammar Axiom T Non terminals 7 041 a_2 Productions T gt s s s s a_1 T gt s a_1 a_i gt s a_2 a_i gt a_2 a2 gt 0 19 GAPT User Manual A Proof systems A 1 LK The rules of LK are listed below Proof trees are constructed top down starting with axioms and with each rule introducing new inferences With the exception of the definition rules the constructors of the rules only allow inferences that are actually valid Note that the rules are presented here as if they always act upon the outermost formulas in the upper sequent but this is only for convenience of presentation The basic constructors actually require the user to specify on which concrete formulas the inference should be performed Apart from those basic constructors there is also a multitude of convenience constructors that facilitate easier proof construction Moreover there are so called macro rules that reduce several inferences to a single command e g introducing quantifier blocks See the API documentation of the individual rules for details Axioms Logical axiom Reflexivity axiom AFA FF axiom TE axiom TEA Theory axiom Logical axioms and
32. theory axioms may only contain atomic formulas Cut TFA A A EFI tut TEFA N a Structural rules Left rules Right rules PEA TEA ATREA PEA o A A TFA cl TFA A A te AJTFA TFA A 20 GAPT User Manual Propositional rules Left rules A B TRA ail ANBTEFA gt ATHA BEET uy AVB T EFA I TKAA a ZA TFA S THA A BSAN Sy A gt B T FA I l Quantifier rules Left rules ALG TFA so VIA T RA ve Aly x PD HA 3 1 IA THA Right rules TAA BEIB 4 T SFA l AAB t THA A B ions TFA AVB ATEFA PELIS ATFAB o TFA ADB Y Right rules TEA Aly z ver TEA VxA f TEA Alt x En EAS C The variable y must not occur free in T A or A The term t must avoid variable capture i e it must not contain free occurrences of variables bound in A Equality rules Left rules s t A T s HI s t A T t 5 O s t A T t H II s t A T s D IL Right rules s t E FII A T s s t5FILAlT s t X HII A T t SE EAT a Each equation rule replaces exactly one occurrence of a term in its auxiliary formula GAPT User Manual Definition rules ATHA A BT T A A def r These definition rules are extremely liberal as they allow the replacement of any formula by any other formula Induction The induction rule applies to arbitrary algebraic data types Let c1 Cn be t
33. tion la Gentzen It can be used as follows first we load a proof p with cuts as in Appendix C gapt gt val p XMLProofDatabaseParser examples simple foli xml gz proofs 0 _2 p at logic gapt proofs lkNew LKProof p25 Vx Vy Px y DQ x y dx dy H0 x y gt P x y CutRule p13 Suc 0 p24 Ant 0 p24 Vx dy P x y VQ x y 3x Jy Q x y D P x y ForallLeftRule p23 Ant 0 dy 4P x y VQ x y b x p23 dy P b y VQ b y dx dy Q x y 5 P x y ExistsLeftRule p22 Ant 0 v y p22 P b v VQ b v 3x Jy Q x y D P x y ExistsRightRule p21 Suc 0 dy Q x y DAP x y b x p21 P b v VQ b v dy 4Q b y D P b y ExistsRightRule p20 Suc 0 Q b y gt P b y v y p20 P b v VQ b v 4Q b v D P b v ImpRightRule p19 Ant 1 Suc 0 12 GAPT User Manual p19 P b v VQ b v Q b v P b v OrLeftRule p16 Ant 0 p18 Ant 1 p18 Q b v Q b v NegLeftRule p17 Suc 0 p17 Q b v and then call the cut elimination procedure gapt gt val q ReductiveCutElimination p q at logic gapt proofs lkNew LKProof p16 Vx Vy P x yDQ y 3x Jy H0 x y gt P x y ForallLeftRule p15 Ant 0 Vy P x y 0 x y b x p15 Vy P b y DQ b y 3x Jy 50 x y gt P x y
34. u can export QF_UF formulas or sequents as SMT LIB benchmarks note that we apply a drastic renaming to the constant symbols in order to support arbitrary even Unicode names in GAPT gapt gt val benchmark typeRenaming constantRenaming SmtLibExporter Sequent f benchmark String set logic QF_UF declare sort t1 0 declare fun f1 t1 Bool declare fun f2 t1 declare fun 3 t1 declare fun f4 t1 assert not gt and or f4 f2 f4 3 and f1 3 1 2 1 4 check sat typeRenaming Map at logic gapt expr TBase at logic gapt expr TBase Map o gt Bool i gt t1 constantRenaming Maplat logic gapt expr Const at logic gapt expr Const Map a gt f4 P gt f1 b gt f2 c gt 3 We can also extract instances for basic equality axioms reflexivity symmetry and congruences from veriT s proof output GAPT User Manual gapt gt val Some expansionSequent VeriT getExpansionSequent Sequent f expansionSequent at logic gapt proofs expansionTrees ExpansionSequent WeakQuantifier Vx Vy x yDy x ArrayBuffer WeakQuantifier Vy a yDy a ArrayBuffer Atom a b DAtom b a b Atom a c DAtom c a c a WeakQuantifier Vx1 Vy1 x1 y1AP x1 gt P y1 ArrayBuffer WeakQuantifier Vy1 c y1AP c DP y1 ArrayBuffer Atom c a AAtom P c DAtom P a a c WeakQuantifier Vy1 b y1AP b DP y1 ArrayBuffer Atom b a AAt
35. with Equality In St phane Demri Deepak Kapur and Christoph Wei denbach editors Automated Reasoning 7th International Joint Conference IJCAR volume 8562 of Lecture Notes in Computer Science pages 240 254 Springer 2014 4 Stefan Hetzl Alexander Leitsch Giselle Reis and Daniel Weller Algorithmic introduction of quantified cuts Theoretical Computer Science 549 1 16 2014 5 Stefan Hetzl Alexander Leitsch and Daniel Weller Towards algorithmic cut introduction In Proceedings of the 18th international conference on Logic for Programming Artificial Intelli gence and Reasoning LPAR 12 pages 228 242 Berlin Heidelberg 2012 Springer Verlag 6 Stefan Hetzl Tomer Libal Martin Riener and Mikheil Rukhaia Understanding Resolution Proofs through Herbrand s Theorem In Didier Galmiche and Dominique Larchey Wendling ed itors Automated Reasoning with Analytic Tableaux and Related Methods TABLEAUX 2013 Proceedings volume 8123 of Lecture Notes in Computer Science pages 157 171 Springer 2013 7 William McCune Prover9 and mace4 manual input files 2005 2010 https www cs unm edu mccune mace4 manual 2009 11A input htm1 8 Dale Miller A Compact Representation of Proofs Studia Logica 46 4 347 370 1987 9 Martin Odersky Lex Spoon and Bill Venners Programming in Scala Artima Inc 2011 10 Gaisi Takeuti Proof Theory North Holland Amsterdam 2nd edition March 1987 11 Daniel Weller CERES in h
Download Pdf Manuals
Related Search