ProofTool: GUI for the GAPT Framework
Contents
1. Partially supported by the project 1383 of the Austrian Science Fund 1GAPT homepage http code google com p gapt CERES homepage PROOFTOOL GUI for the GAPT Framework Dunchev et al 2 Preliminaries In this section some basic terms which will be used through the paper are presented We start from the CERES system and a comparison of PROOFTOOL with its old prototype both programs are called prooftool but to avoid confusion the old one is written with a verbatim font 2 1 The CERES System GAPT was conceived to replace and expand the scope of the CERES system which consists of the programs ceres hlk and prooftool The CERES system uses Prover9 to refute clause sets which is a vital step of the CERES method CERES is a cut elimination method by resolution Its basic data structures are struct characteristic clause set and projection set The struct is a clause term obtained from a proof with cuts and the characteristic clause set is a clause set obtained by evaluation of a struct Projections are cut free parts of a proof obtained by skipping all inferences going into cuts In this paper we refer to these objects as the data structures of the CERES method The system works in the following way First the user enters a formal proof into the CERES system using the handy L H language Then the program hlk compiles this formalization to an XML file which is used as input for the ceres program In the next step ceres is2. 599 656 BLOO Matthias Baaz and Alexander Leitsch Cut elimination and redundancy elimination by resolution Journal of Symbolic Computation 29 2000 no 2 149 176 DLRW12 C Dunchev A Leitsch M Rukhaia and D Weller About Schemata And Proofs web page 2010 2012 http www logic at asap HLW11 Stefan Hetzl Alexander Leitsch and Daniel Weller CERES in higher order logic Annals of Pure and Applied Logic 162 2011 no 12 1001 1034 HLW12 Towards algorithmic cut introduction LPAR 2012 pp 228 242 HLWWP08 Stefan Hetzl Alexander Leitsch Daniel Weller and Bruno Woltzenlogel Pa leo Herbrand sequent extraction Intelligent Computer Mathematics Serge Autexier John Campbell Julio Rubio Volker Sorge Masakazu Suzuki and Freek Wiedijk eds Lecture Notes in Computer Science vol 5144 Springer Berlin 2008 pp 462 477 Mai09 Ingo Maier The scala swing package http www scala lang org sid 8 2009 McC10 W McCune Prover9 and mace4 http www cs unm edu mccune prover9 2005 2010 OSV 10 Martin Odersky Lex Spoon and Bill Venners Programming in Scala A comprehensive step by step guide 2nd ed Artima Inc 2010 10
3. al guage would be convenient One solution is to use XTex and create such an editor using the grammar of the proof input language An advantage of the grammar is that it is easy to give exact lines where the parsing of a file fails because of a syntactic error 4 ProofTool From a User Perspective PROOFTOOL is a graphical user interface used to display objects generated by the GAPT system These objects are trees proofs sequents formulas etc Below we describe features of PROOFTOOL related to these objects 4 1 Input Output PROOFTOOL supports different kinds of parsers one for lks files and two for different XML formats ceres xml and simple rml possibly in gzipped form As we saw in the previous sections lks files are used to input schematic proofs The ceres xml format is used for proofs in first and higher order sequent calculus Simple xml format is a general format where one can input arbitrary tree like proofs e g natural deduction tableaux etc So far it is used to communicate with RegSTAB ACP10 There are disadvantages of using the simple xml format since it is a very general format structural details about the proof are absent For instance the leaves of a proof will be displayed simply as the strings which occur in the XML file instead of an easier readable TEX rendering This also means some advanced features of prooftool might not work Basic features like zooming are not affected but certain views might not b
4. containing a higher order expression of type HOLEXPRESSION which also includes first order and schema formulas is rendered by JLATEXMATH Other types of vertices are displayed simply as their Scala string representation which often suffices since the Unicode character set used includes Greek letters as well as other logical symbols PROOFTOOL strongly profits from the SCALA SWING wrapper library which simplifies event handling significantly Since there are only PUBLISHER and REACTOR elements in stead of Java s complicated event handling mechanism for instance menu items only need to listen to the PROOFTOOLPUBLISHER to adjust their activation status accordingly In the case a new file is loaded or the proof database is dynamically changed the PROOFD BCHANGED event is issued Since also the View gt View Proof View gt View Clause List and View gt View Term Tree menus listen to this event they can refresh their list of MENUITEMs 6 Future Work This paper presented a graphical user interface for the GAPT framework It is able to display various new and legacy proof formats even if they are tailored towards humans PROOFTOOL is also flexible enough to render sequent calculus and resolution proofs as well as other tree like structures in appealing ways and acts as a graphical shell to the functionality of GAPT 5 JLATEXMATH homepage http Scilab homepage PROOFTOOL GUI for the GAPT Framework Dunchev et al In the future
5. has several reasons A PROOF is only a directed acyclic graph so additional arrows for shared structures would be necessary Apart from sequent calculus proofs at the moment only resolution proofs need to be displayed These are still easily readable in TREE form which is easily obtained from the DAG 4X Text homepage http www eclipse org Xtext PROOFTOOL GUI for the GAPT Framework ile Edit View LK Proof LKS Proof Help Schematic S tru ct AA Fi x AN penn OO 7N x XK CJ IAN nM a xK X 8 LAX ory ee S x uK O x X LEA aN S L xxx e oe xX KX oe gt NANI N ANAA x x xx x fe li blew x x en S x x 4 Figure 3 Tree in PROOFTOOL leaves are hidden Dunchev et al In general proofs in the GAPT system are sequent like proofs and an example how they are displayed in PROOFTOOL is shown on Figure 4 File Edit View LKProof LKS Proof Help psi k Pri H Pri eri ae hike Peyi OP H Pk 2 H Pro Po NOB V Pai H Peni a ai i 0 Prt Pit V Prez H Pise k cut P NORV Pat Pesi V Pisa H Peo i 0 k Pi Pisi V Pisa A AP V Paa A Piai V Pes H Per i 0 k k Py A APiV Past A Piei V Pes ACOP V Paa A Pesi V Pisa H 4 i 0 i 0 k Py A APiV Bai A Pisi V Pes2 E Pea i 0 1 k l AGRY Pa
6. not be used as input Since the modification of the ceres xml parser to accommodate this drawback is quite straightforward we expect to add this feature in the near future Most of the other features of GAPT are related to the CERES method It provides data structures for schematic first order and higher order formulas as well as different sequent and resolution calculi Many algorithms like regularization skolemization matching and PROOFTOOL GUI for the GAPT Framework Dunchev et al various unification algorithms are contained Their use is shared with the interactive theorem prover TAP which is also part of the system Another part are the libraries connecting external theorem provers like Vampire and Prover9 The calculation of the struct of the characteristic clause set and of the proof projections now form the heart of GAPT It is also accompanied by methods to extract the Herbrand Sequent and serves as a test bed for cut introduction methods currently under development 3 Proof Input Language Since proofs are the main input for the GAPT system a comfortable proof input language is important Unfortunately the handy LK language has several shortcomings The first and major one is that a user cannot input a given formal proof as it is because originally handy LK was designed for interactive proof search Second it can not directly treat proof schemata Although it allows recursively defined input proofs it can output only user spec
7. ProofTool GUI for the GAPT Framework Cvetan Dunchev Alexander Leitsch Tomer Libal Martin Riener Mikheil Rukhaia Daniel Wellert Bruno Woltzenlogel Paleo cdunchey leitsch shaolin riener mrukhaia weller bruno logic at Institute of Computer Languages E185 Institute of Discrete Mathematics and Geometry F104 Vienna University of Technology Abstract This paper describes an implementation and the features of a proof viewer which fulfills the role of a graphical user interface to the General Architecture for Proof Theory GAPT framework It contains methods to render classical and schematic sequent calculus proofs as well as resolution proofs and other tree like structures in a flexible way Additional emphasis is put on the schema proof input format for the end user which should be as user friendly as possible 1 Introduction GAPT General Architecture for Proof Theory is a framework that aims at provid ing data structures algorithms and user interfaces for analyzing and transforming formal proofs GAPT was conceived to replace and expand the scope of the CERES systenq beyond the original focus on cut elimination by resolution for first order logic BLOO Through a more flexible implementation based on basic data structures for simply typed lambda calculus and for sequent and resolution proofs in the hybrid functional object oriented language Scala OSV10 GAPT has already allowed the implementation of the generalization of
8. e available To open an input file users should use the corresponding menu item of the File menu or type the Ctr1 0 key combination In PROOFTOOL there are several exporters for objects of the GAPT system One of them is the already mentioned ceres xml exporter which can save proofs sequent lists and definition lists in an wml file This is done from the menu items save proof as XML which saves currently displayed proof and save all as XML which saves the whole database of the File menu or by typing the Ctrl P and Ctr1 S key combinations respectively There are also several sequent list exporters which will be discussed later in this section 4 2 Trees TREEs are binary trees in the system and they are displayed upside down see Figure 3 The user can manipulate the size of the tree by hiding showing some branches or leaves This is done by calling the corresponding menu items of the Edit menu or by clicking on the vertex that should be hidden shown For tree like objects like the clause term or the projection term the system contains transformations to trees A simple example is a directed acyclic graph where the corre sponding tree just has duplicates of the shared structures 4 3 TreeProofs A TREEPROOF is also a binary tree in the GAPT system which represents tree like proof It is a TREE which is also a PROOF This means that we can expect that nodes are labeled with sequents The decision to display TREEPROOFs instead of PROOFs
9. ement of a list is displayed in a single line Lines are separated with semicolons The most commonly occurring lists in the GAPT system are sequent lists and definition lists An example how sequent lists are displayed is shown on Figure File Edit View LKProof LKS Proof Help sequentList 0 81 k s lt k p s p s1 L mo 0 so p s1 to p nat 173 A nat473 lt k H 0 no to no to to p nat473 r nat 473 lt k H Figure 5 List in PROOFTOOL In the GAPT system we have several exporters for sequent lists and PROOFTOOL allows to export them in two different formats either in tex or tptp files This is done by calling the corresponding menu items of the File menu or by typing the key combinations Ctr1 E or Ctrl T respectively 4 5 Features Under Development In this subsection two features are discussed which we find very useful They are currently under development The first one is searching and the second one is hiding of structural PROOFTOOL GUI for the GAPT Framework Dunchev et al rules in a proof Searching is very useful when one has to deal with huge proofs or other objects which is often the case in our research So we decided to have a feature that will allow us to search in objects displayed by PROOFTOOL Currently it is done in the following way a user calls the Edit gt Search menu item or the Ctrl F key combination and t
10. i P H Pez 4 psi 1 Figure 4 Proof in PROOFTOOL There are two kinds of sequent like proofs in GAPT first and higher order sequent cal culus proofs LK proofs and schematic sequent calculus proofs LKS proofs In PROOFTOOL there are menus LK Proof and LKS Proof containing the possible operations for these proofs respectively The available menu items are the following e From the LK Proof menu teristic clause set Compute the data structures of the CERES method such as struct and charac PROOFTOOL GUI for the GAPT Framework Dunchev et al Apply reductive cut elimination Gentzen s method e From the LKS Proof menu Compute the data structures of the Schematic CERES method such as schematic struct schematic characteristic clause set and schematic projection term Compute the instance of a schematic proof for the number given by the user e From the Edit menu Hide sequent context for each rule in the proof show only the auxiliary formulas used in the rule Mark cut ancestors highlight all ancestors of all cut formulas occurring in the proof Extract cut formulas extract list of all cut formulas This is not everything that the GAPT system provides but the other functionalities will be added to PROOFTOOL on a by need basis 4 4 Lists Lists are very important data structures and it is worthy to have specialized handling for them In PROOFTOOL each el
11. ified instances of it But transformations of schematic proofs require that the schema is kept throughout the whole process since the output format is again a schematic proof These drawbacks rectified the definition of a new language which is called proof input language here The proof input language is designed to write schematic proofs in a form which is both easily human and machine readable It is simple enough that an input proof can be written in any text editor To differentiate it from other text files the extension lks is used The full description of the grammar of the language as well as of the formal calculus can be found in DLRW12 One lks file must contain at least one proof definition which has the pattern given on Figure For an inductive proof definition the base block describes the base case and the step block describes the recursive case The ids are arbitrary labels that are unique within blocks i e the same labels can be used in the definition of base and step cases and rules are tuples consisting of the rule s name the ids of the premises and of the auxiliary formulas proof name proves sequent base id rule idn rulen root rul n 1 step id rule idm rulem root rulem 1 Figure 2 Proof syntax of proof input language As the language would profit from syntax highlighting having an editor for this lan PROOFTOOL GUI for the GAPT Framework Dunchev et
12. investigations Therefore it contains an implemen tation of the basic data structures and algorithms for the schematic CERES method such as the schematic struct the schematic characteristic clause set the schematic projection term and their extraction from proof schemata 2 3 The GAPT System GAPT is a framework that aims at providing data structures algorithms and user inter faces for analyzing and transforming formal proofs Although it is a quite complex system here we focus on features that are integrated in PROOFTOOL We start our discussion from parsers and exporters There are several input formats parsed by the GAPT system but the most important ones are the schematic proof input language the ceres rml format and a less restrictive so called simple xml format The proof input language will be discussed in the next section Simple xml is a simplified version of ceres xml which is general enough to communicate with other systems While ceres xml requires that the proof is a sequent calculus proof there is no such restriction in the simple xml format Therefore it can be used for exchanging any tree like proofs with other systems like it was done with RegSTAB The current output format slightly differs from the ceres xml format The reason for this is that the ceres xml format is tailored to a sequent calculus with permutation rules and the GAPT system represents sequents as multisets instead Therefore at the moment the output XML can
13. oot node at the top and then creates new DRAWTREE instances for the child trees For a binary node the branches of the tree are rendered side by side on a frame and a unary node shows the branch in the center The root is connected to its children by straight lines DRAWPROOF also extends the BORDERPANEL class and behaves similar to DRAWTREE The difference is that the desired output looks like a sequent calculus proof This means that while DRAWTREE puts the vertex at the top and the branches below DRAWPROOF puts the vertex at the bottom and the branches on top of it Then it draws horizontal lines between vertices and puts the rule names next to the lines DRAWLIST extends the GRIDPANEL class having only one column and puts each element of the list in a separate cell In PROOFTOOL a sequent is displayed by a FLOWPANEL which contains the represen tation of each formula as a separate LABEL To handle formulas the decision was made to use JLATEXMaTH It is a Java API which displays mathematical formulas written in ATX as images Although it is used in GUI of Scilalf having an image for every formula is quite memory consuming For each formula displayed a label is created Then the formula is transformed into a BTEX string and rendered using JUATEXMATH The resulting image is assigned as an icon to the label Since this rendering is expensive we use it only when necessary and display simple string representations otherwise For example any vertex
14. own decidable and a tableau calculus STAB was defined and implemented ACP10 RegSTAB is a STAB prover that refutes regular for mula schemata It outputs the tableau refutation in an XML file which can be read by PROOFTOOL 3Handy LK syntax nttp www logic at hlk handy syntax pdf PROOFTOOL GUI for the GAPT Framework Dunchev et al Features PROOFTOOL prooftool Zooming scrolling Yes Yes Display first and higher order proofs Yes Yes Display sequent lists Yes Yes Parse ceres XML export in tex Yes Yes Export in tptp Yes No Proof schemata and related features Yes No Trees and related features Yes No Display definition lists Yes No Marking cut ancestors extracting cut formulas Yes No Hiding sequent context Yes No Searching Yes No Hiding structural rules Yes No Split unsplit Substitute unsubstitute No Yes Figure 1 PROOFTOOL vs prooftool By proof schemata we mean schematic sequent calculus proofs In this calculus sequents are multisets of formula schemata and proofs are defined in a recursive way The rules are similar to those of a usual sequent calculus but they operate on formula schemata As a special axiom rule proof links connect recursive instances of other proofs A detailed description of schematic sequent calculus can be found in DERW12 Since the CERES method for proof schemata is currently under development the GAPT system is used for practical
15. shown on Figure 6 SimpleSwingApplication O FileParser Launcher extends GridBagPanel aa N DrawTreeProof extends BorderPanel D Draw Tree extends BorderPanel DrawList extends GridPanel DrawSequent y jLatexMath Figure 6 Architecture of PROOFTOOL SCROLLPANE has a component called LAUNCHER which extends GRIDBAGPANEL and takes the following parameters e A pair STRING ANYREF where ANYREF is an object that should be displayed and STRING is a name of the object The object has TITLEDBORDER around it and the name is the title PROOFTOOL GUI for the GAPT Framework Dunchev et al e An INT which is a size of font that is used to display an object Thanks to such a general design the basic feature zooming can be applied to all objects easily by calling the zoom in and zoom out menu items from the View menu or by the Alt t and Alt key combinations respectively When an object is passed to LAUNCHER it uses Scala s matching mechanism to recognize its structure and instantiates the corresponding class responsible for the drawing of the object Basically LAUNCHER differentiates between three kinds of objects trees proofs and lists The rendering classes are DRAWTREE DRAWPROOF and DRAWLIST respectively DRAWTREE extends the BORDERPANEL class and displays a tree in the following way A leaf node just renders the vertex whereas an inner node draws the r
16. the cut elimination by resolution method to proofs in higher order logic and to schematic proofs DLRW12 Furthermore methods for structuring and compressing proofs such as cut introduction and Herbrand Sequent Extrac tion are being implemented The GAPT system has a command line interface CLI that allows a user to access the capabilities of the system e g to create and manipulate proofs But such an interface is not suited for the visualization of proofs when viewing proofs which are large trees or DAGs more sophisticated user interaction scrolling viewing hiding of information which can not provided by a CLI is required Hence a proof viewer called PROOFTOOL was implemented to allow for such a more sophisticated visualization While it is possible to call a PROOFTOOL frame from the CLI to visualize a particular piece of data the aim is to extend PROOFTOOL to become a stand alone graphical user interface for GAPT For the time being PROOFTOOL gives access to most of GAPT s features It is constantly being extended towards becoming a fully fledged GUI for the GAPT system The rest of the paper is organized as follows Section 2 describes the GAPT system in more detail and gives some basic understanding of the terms used in the paper In Section Bla language for the input of schematic proofs is presented and in Sections 4 and 5 PROOFTOOL is described in detail The final section discusses some future implementations and improvements
17. the proof input language will be extended to first order schematic proofs Also the input language should unify parsing of schematic and classical sequent calculus proofs It is planned to change the parser such that it automatically inserts weakening and contraction rules left out by the user which would ease the proof specification process Regarding PROOFTOOL more commands already available in the command line in terface e g skolemization regularization Herbrand sequent extraction theorem prover integration etc will be added to the GUI Also efficiency issues will be tackled since at the moment 20MB of stack and 2GB of heap memory barely suffice to run GAPT s algo rithms on formulations of real mathematical proofs like the formulation of Fiirstenberg s proof of the infinity of primes or a schematic formulation of an n bit adder Finally a user manual and an on line help system are in planning References ACP09 Vincent Aravantinos Ricardo Caferra and Nicolas Peltier A schemata cal culus for propositional logic Automated Reasoning with Analytic Tableaux and Related Methods Lecture Notes in Computer Science vol 5607 Springer 2009 pp 32 46 ACP10 RegSTAB A SAT Solver for Propositional Iterated Schemata In ternational Joint Conference on Automated Reasoning 2010 pp 309 315 ACP11 Decidability and undecidability results for propositional schemata Journal of Artificial Intelligence Research 40 2011
18. used to perform the following steps e skolemize the proof e calculate the characteristic clause set e call an external first order resolution prover and calculate a resolution refutation of the characteristic clause set e calculate the proof projections and generate the output original proof Atomic Cut Normal Form ACNF characteristic clause set Herbrand sequent etc The output of ceres is again its input XML format Now the program prooftool is used to visualize the formal proofs obtained by ceres In the following we will call the XML format used during these steps as ceres xml format PROOFTOOL has several advantages over the old prototype First it can display general tree like structures such as the struct with varying graphical output In contrast to that prooftool can only display sequent calculus proofs so for instance a list of sequents is shown as a proof with unary inferences which is quite counter intuitive Second PROOFTOOL is flexible enough to handle proof schemata as objects This is necessary since the output of the CERES method is again a proof which means that if a proof schema is transformed not only an instance should be displayed but the schema itself Third it supports more input and output formats than the old prototype A full comparison is given on Figure I 2 2 Proof Schemata Formula schemata were introduced and investigated in ACPO9 ACPI A subclass called regular schemata was identified and sh
19. ypes possibly latex string representation of the object s he wants to search Then this string is searched in the string representation of the displayed object and if found the corresponding part is highlighted A problem occurring during search is that the string representation of a node might be quite different from its rendering Let us consider the search in the proof displayed in Figure After typing cut in the search dialog PROOFTOOL will find the rule name and color it green If the search is for the formula P 1 then exactly the BTEX representation neg P_ k 1 needs to be entered Counter intuitively the search for neguuP_ k 1 will fail even if the rendered formula looks the same Some remedies for the problems are already worked on but there is no straightforward solution maintaining the flexibility of the input formats Hiding structural rules is also very useful to shorten the size of proofs In most of the cases structural rules do not contain any valuable information and they can be hidden for the user The Edit gt Hide Structural Rules menu item allows access to this feature although it sometimes hides too few inferences Investigation into this matter is still in progress 5 Implementation Details PROOFTOOL is implemented using the SCALA SWING library It is a SIMPLESWING APPLICATION and consists of one frame which contains a MENUBAR and a SCROLLPANE We continue with a brief description of the architecture of PROOFTOOL
Download Pdf Manuals
Related Search