Hets User Guide
Contents
1. 2002 Geoff Sutcliffe and Christian B Suttner Evaluating general purpose au tomated theorem proving systems Artificial Intelligence 131 1 2 39 54 2001 Geoff Sutcliffe and Christian B Suttner The state of CASC AI Commu nications 19 1 35 48 2006 http www xemacs org People index html XEmacs Available at http www xemacs org Paolo Torrini Christoph Lith Christian Maeder and Till Mossakowski Translating Haskell to Isabelle Isabelle workshop at CADE 21 2007 Jan Oliver Wallgriin Lutz Frommberger Frank Dylla and Diedrich Wolter SparQ user manual v0 6 2 University of Bremen 2006 C Weidenbach U Brahm T Hillenbrand E Keen C Theobalt and D Topic SPASS version 2 0 In Andrei Voronkov editor Automated Deduction CADE 18 volume 2392 of Lecture Notes in Computer Science pages 275 279 Springer Verlag July 27 30 2002 27 44 Jiirgen Zimmer and Serge Autexier The MathServe System for Seman tic Web Reasoning Services In U Furbach and N Shankar editors 3rd IJCAR LNCS 4130 Springer 2006 282. Jones editor Haskell 98 Language and Libraries The Revised Report Cambridge 2003 also J Funct Programming 13 2003 Simon Peyton Jones Mark Jones and Erik Meijer Type classes exploring the design space In Haskell Workshop 1997 Alexandre Riazanov and Andrei Voronkov The design and implementation of VAMPIRE AI Communications 15 2 3 91 110 2002 M Roggenbach CSP CASL a new integration of process algebra and algebraic specification Theoretical Computer Science 354 1 42 71 2006 L Schroder T Mossakowski and C Maeder HasCasi Integrated functional specification and programming Language summary Available at http www informatik uni bremen de agbkb forschung formal_ methods CoFI HasCASL 2003 Lutz Schroder Higher order and reactive algebraic specification and development Summary of papers constituting a cumulative habilita tion thesis available under http www informatik uni bremen de 1schrode papers Summary pdf 2005 Lutz Schr der The HasCASL prologue categorical syntax and semantics of the partial A calculus Theoret Comput Sci 353 1 25 2006 Lutz Schroder and Till Mossakowski HASCASL Towards integrated specification and development of Haskell programs In H Kirchner and C Ringeissen editors Algebraic Methods and Software Technology 9th International Conference AMAST 2002 Saint Gilles les Bains Reunion Island France Proceedings LNCS Vol 2422 pages 99 116 Springer
3. g error handling is ignored For technical reasons a logic is tagged with a unique identifier type lid which is a singleton type the only purpose of which is to determine all other type components of the given logic In Haskell jargon the interface is called a multiparameter type class with func tional dependencies 31 The Haskell interface for logic translations is realised similarly The logic independent modules in HETS can be found in the right half of Fig 8 These modules comprise roughly one third of Hers 100 000 lines of Haskell code The heterogeneous parser transforms a string conforming to the syntax in Fig 1 to an abstract syntax tree using the Parsec combinator parser 15 Logic and translation names are looked up in the logic graph this is necessary to be able to choose the correct parser for basic specifications Indeed the parser has a state that carries the current logic and which is updated if an explicit specification of the logic is given or if a logic translation is encountered in the latter case the state is set to the target logic of the translation With this it is possible to parse basic specifications by just using the logic specific parser of the current logic as obtained from the state 21 class Logic lid sign morphism sentence basic_spec symbol_map lid gt sign morphism sentence basic_spec symbol_map where identity lid gt sign gt morphism compose lid gt morphism gt
4. hence supports the Haskell module system By contrast in HETCAsL libraries ending with het the logic Haskell has to be chosen explicitly and the CAsL structuring syntax needs to be used library Factorial logic Haskell spec Factorial fac Int gt Int fac n foldl 1 1 n end Note that according to the Haskell syntax Haskell function declarations and definitions need to start with the first column of the text 7 Development Graphs Development graphs are a simple kernel formalism for heterogeneous struc tured theorem proving and proof management A development graph consists of a set of nodes corresponding to whole structured specifications or parts thereof and a set of arrows called definition links indicating the dependency of each involved structured specification on its subparts Each node is associated with a signature and some set of local axioms The axioms of other nodes are inherited via definition links Definition links are usually drawn as black solid arrows denoting an import of another specification Complementary to definition links which define the theories of related nodes theorem links serve for postulating relations between different theories Theo rem links are the central data structure to represent proof obligations arising in formal developments Theorem links can be global drawn as solid arrows or local drawn as dashed arrows a global theorem link postulates that all axioms of
5. morphism gt morphism dom codom lid gt morphism gt sign parse_basic_spec lid gt String gt basic_spec parse_symbol_map lid gt String gt symbol_map parse_sentence lid gt String gt sentence empty_signature lid gt sign basic_analysis lid gt sign gt basic_spec gt sign sentence stat_symbol_map lid gt sign gt symbol_map gt morphism map_sentence lid gt morphism gt sentence gt sentence provers lid gt sign sentence gt sentence gt Proof_status cons_checkers lid gt sign sentence gt Proof_status class Comorphism cid lidi signi morphismi sentence1l basic_specl symbol_map1i lid2 sign2 morphism2 sentence2 basic_spec2 symbol_map2 cid gt lid1 1id2 where sourceLogic cid gt lidi targetLogic cid gt 1id2 map_theory cid gt signi sentence1 gt sign2 sentence2 map_morphism cid gt morphism1 gt morphism2 Figure 7 The basic ingredients of logics and logic comorphisms 22 Architecture of the heterogeneous tool set Hets Tools for specific logics Logic graph Tools for heterogeneous specifications Haskell x a Isabelle Abstract syntax Fal Parser Signature anaes soon CoCASL Static Analysis Interfaces yy Fl Global eer p Pn J Nan XML Aterm Pa CASL DL XML pm ModalCASL t OWL DL Halerogansou Rewriters el development graphs Tea Heterogeneous inference engine Decompositi
6. the most appropriate ATP system upon a clas sification based on the SPCs and on a training with the library Thousands of Problems for Theorem Provers TPTP 44 The TPTP format has been introduced by Sutcliffe and Suttner for the annual competition CASC 39 and 19 provides a unified syntax for untyped FOL with equality but without any sym bol declaration 10 2 Isabelle ISABELLE 29 is an interactive theorem prover which is more powerful than ATP systems but also requires more user interaction ISABELLE has a very small core guaranteeing correctness and its provers like the simplifier or the tableaux prover are built on top of this core Further more there is over fifteen years of experience with it and several mathematical textbooks have been partially verified with ISABELLE ISABELLE is a tactic based theorem prover implemented in standard ML The main ISABELLE logic called Pure is some weak intuitionistic type theory with polymorphism The logic Pure is used to represent a variety of logics within ISABELLE one of them being Hot higher order logic For example logical implication in Pure written gt also called meta implication is different from logical implication in Hot written gt also called object implication It is essential to be aware of the fact that the ISABELLE Hot logic is differ ent from the logics that are encoded into it via comorphisms Therefore the formulas appearing in subgoals of proof
7. www informatik uni bremen de uDrawGraph en Tcl Tk graphics widget system http www scriptics com software tcltk SPASS theorem prover http spass mpi sb mpg de ISABELLE theorem prover http www cl cam ac uk Research HVG Isabelle X Emacs editor for Isabelle must be installed manually 2 If you do not have Sun Java you can just download the hets binary You have to unpack it with bunzip2 and then put it at some place coverd by your PATH You also have to install the above mentioned software and set several environment variables as explained on the installation page 3 If you want to compile HETs from the sources please follow the link Hets source code and information for developers on the HETs web page down load the sources as tarball or from svn and follow the instructions in the INSTALL file 5 Analysis of Specifications Consider the following CAsL specification spec STRICT_PARTIAL_ORDER sort Elem pred _ lt _ Elem x Elem Va y z Elem e z lt 2 strict er lt y gt y lt z asymmetric er lt yAy lt 2 gt uK lt z transitive Note that there may exist x y such that neither x lt y nor y lt x end Hers can be used for parsing and checking static well formedness of specifi cations Let us assume that the example is in a file named Order cas1 actually this file is provided with the Hers distribution Then you can check the well formedness of the specification by ty
8. 002 Santa Margherita Ligure Italy Proceedings LNCS Vol 2309 pages 2 17 Springer 2002 T Berners Lee J Hendler and O Lassila The Semantic Web Scientific American May 2001 M Bidoit and P D Mosses Casi User Manual volume 2900 of LNCS Springer 2004 Free online version available at http www cofi info Patrick BLackburn Maarten de Rijke and Yde Venema Modal Logic Cambridge University Press Cambridge England 2001 M G J van den Brand H A de Jong P Klint and P Olivier Efficient annotated terms Software Practice amp Experience 30 259 291 2000 Free Software Foundation Emacs Available at http www gnu org software emacs emacs html J Goguen and G Rosu Institution morphisms Formal aspects of comput ing 13 274 307 2002 J A Goguen and R M Burstall Institutions Abstract model theory for specification and programming Journal of the Association for Computing Machinery 39 95 146 1992 Predecessor in LNCS 164 221 256 1984 Sonja Gr ning Beweisunterstiitzung fiir HasCASL in Isabelle HOL Mas ter s thesis University of Bremen 2005 Diplomarbeit Marc Herbstritt zChaff Modifications and extensions report00188 Insti tut fir Informatik Universitat Freiburg July 17 2003 Thu 17 Jul 2003 17 11 37 GET Michael Kohlhase OMDoc An Open Markup Format for Mathematical Documents version 1 2 volume 4180 of Lecture Notes in Computer Sci ence Springer 2006 Daan
9. ETs support for the different languages that in the future HETS might be applied to itself The definitive reference for Haskell is 30 see also www haskell org CspCASL 33 is a combination of Cast with the process algebra CSP ConstraintCASL is an experimental logic for the specification of qualitative constraint calculi OWL DL is the Web Ontology Language OWL recommended by the World Wide Web Consortium W3C http www w3c org It is used for knowl edge representation and the Semantic Web 5 Hets calls an external OWL DL parser written in JAVA to obtain the abstract syntax for an OWL file and its imports The JAVA parser is also doing a first analysis classify ing the OWL ontology into the sublanguages OWL Full OWL DL and OWL Lite Hets only supports the last two more restricted variants The structuring of the OWL imports is displayed as Development Graph CASL DL 16 is an extension of a restriction of Cast realizing a strongly typed variant of OWL DL in Cast syntax It extends Cast with cardi nality restrictions for the description of sorts and unary predicates The restrictions are based on the equivalence between CASL DL OWL DL and SHOIN D Compared to Cast only unary and binary predicates prede fined datatypes and concepts subsorts of the topsort Thing are allowed It is used to bring OWL DL and Cast closer together Propositional is classical propositional logic with the zChaff SAT solver 13 connected t
10. Hets User Guide Version 0 85 Till Mossakowski Christian Maeder Klaus L ttich DFKI Lab Bremen Bremen Germany Comments to hets informatik uni bremen de or to hets users informatik uni bremen de the latter needs subscription to the mailing list February 12 2009 1 Introduction The Heterogeneous Tool Set Hers is the main analysis tool for the specifica tion language heterogeneous CAs Heterogeneous Cast HETCASL combines the specification language Cast 6 28 with CAs extensions and sublanguages as well as completely different logics and even programming languages such as Haskell HETCast see Fig 1 for a simple subset extends the structuring mech anisms of Cast Basic specifications are unstructured specifications or modules written in a specific logic The graph of currently supported logics and logic translations the latter are also called comorphisms is shown in Fig 2 and the degree of support by HETs in Fig 3 With heterogeneous structured specifications it is possible to combine and rename specifications hide parts thereof and also translate them to other logics Architectural specifications prescribe the structure of implementations Specifi cation libraries are collections of named structured and architectural specifica tions HETs consists of logic specific tools for the parsing and static analysis of the different involved logics as well as a logic independent parsing and static analysis tool fo
11. Leijen and Erik Meijer Parsec Direct style monadic parser combi nators for the real world Technical report UU CS 2001 35 K L ttich T Mossakowski and B Krieg Briickner Ontologies for the Se mantic Web in CASL In Jos Fiadeiro editor Recent Trends in Algebraic Development Techniques 17th International Workshop WADT 2004 vol ume 3423 of Lecture Notes in Computer Science pages 106 125 Springer Berlin http www springer de 2005 25 17 18 19 20 21 22 23 24 25 26 27 28 29 Klaus Liittich and Till Mossakowski Reasoning Support for CASL with Automated Theorem Proving Systems WADT 2006 Springer LNCS to appear T Mossakowski HetCASL heterogeneous specification language sum mary 2004 T Mossakowski ModalCASL specification with multi modal logics lan guage summary 2004 T Mossakowski Heterogeneous specification and the heterogeneous tool set Habilitation thesis University of Bremen 2005 T Mossakowski S Autexier and D Hutter Development graphs proof management for structured specifications Journal of Logic and Algebraic Programming 67 1 2 114 145 2006 Till Mossakowski CAsL From semantics to tools In S Graf and M Schwartzbach editors Tools and Algorithms for the Construction and Analysis of Systems 6th International Conference TACAS 2000 Berlin Germany Proceedings LNCS Vol 1785 pages 93 108 Springer 2000 T
12. as been developed by Serge Autexier and Dieter Hutter We also want to thank Agn s Arnould Thibaud Brunet Pascale LeGall Kathrin Hoffmann Katiane Lopes Stefan Merz Maria Martins Moreira Christophe Ringeissen Markus Roggenbach Dmitri Schamschurko Lutz Schr der Kon stantin Tchekine and Stefan W lfi for giving feedback about Cars HOL CASL and Hers Finally special thanks to Christoph L th and George Russell for help with connecting HETs to their UniForM workbench References 1 D Aspinal S Berghofer P Callaghan P Courtieu C Rafalli and M Wenzel Emacs Proof General Available at http proofgeneral inf ed ac uk 2 David Aspinall Proof general A generic tool for proof development In Susanne Graf and Michael I Schwartzbach editors TACAS volume 1785 of Lecture Notes in Computer Science pages 38 42 Springer 2000 3 S Autexier D Hutter T Mossakowski and A Schairer The development graph manager Maya system description In H Kirchner and C Ringeis sen editors Algebraic Methods and Software Technology 9th International 24 12 13 Ta JA 15 16 Conference AMAST 2002 Saint Gilles les Bains Reunion Island France Proceedings LNCS Vol 2422 pages 495 502 Springer 2002 Serge Autexier and Till Mossakowski Integrating HoL CASL into the development graph manager Maya In A Armando editor Fron tiers of Combining Systems 4th International Workshop FroCoS 2
13. d to subscribe to the list before you can send a mail But note that subscription is very easy If your favourite logic is missing in HETs please tell us hets users informatik uni bremen de We will take account your feedback when deciding which logics and proof tools to integrate next into HETs Help with integration of more logics and proof tools into HETs is also welcome Acknowledgement The heterogeneous tool set HETS would not have possible without cooperation with many people Besides the authors the following peo ple have been involved in the implementation of Hers Katja Abu Dib Mihai Codescu Carsten Fischer Jorina Freya Gerken Rainer Grabbe Sonja Groning Daniel Hausmann Wiebke Herding Hendrik Iben Cui Ken Jian Heng Jiang Anton Kirilov Tina Krausser Martin K hl Mingyi Liu Dominik L cke Ma ciek Makowski Immanuel Normann Razvan Pascanu Daniel Pratsch Felix Reckers Markus Roggenbach Pascal Schmidt Paolo Torrini Ren Wagner Jian Chun Wang and Thiemo Wiedemeyer Herts has been built based on experiences with its precursors CATS and Maya The Cast Tool Set Cats 22 24 provides parsing and static analysis for Cast It has been developed by the first author with help of Mark van den Brand Kolyang Bartek Klin Pascal Schmidt and Frederic Voisin Maya 4 3 is a proof management tool based on development graphs MAYA only supports development graphs without hiding and without logic transla tions Maya h
14. e effort of integrating CASL extensions quite moderate CoCASL 27 is a coalgebraic extension of CAsL suited for the specification of process types and reactive systems The central proof method is coinduc tion ModalCASL 19 is an extension of Cast with multi modalities and term modalities It allows the specification of modal systems with Kripke s possible worlds semantics It is also possible to express certain forms of dynamic logic HasCASL is a higher order extension of CAs allowing polymorphic datatypes and functions It is closely related to the programming language Haskell and allows program constructs being embedded in the specification An overview of HASCASL is given in 37 the language is summarized in 34 the semantics in 36 35 Haskell is a modern pure and strongly typed functional programming lan guage It simultaneously is the implementation language of HETs such Figure 2 Graph of logics currently supported by Hers The more an ellipse is filled with green the more stable is the implementation of the logic Blue indicates a prover supported logic Language Parser Static Analysis Prover CASL x x CoCAsL x x ModalCAsL x x HaAsCASL x x Haskell x x Csp CasL x ConstraintCAsL x x CasL DL x OWL DL basic x x OWL DL structure x x Propositional x x x SoftFOL x ISABELLE x Figure 3 Current degree of H
15. er with the negation of the conjecture have no satisfying assignment to prove theorems with zChaff That is why you see the result UNsaT in the proof details if a theorem has been proved to be true zChaff uses the same ATP GUI as the provers for SoftFOL ref to section 10 1 zChaff does not accept any options 20 apart from the time limit The current integration of zChaff into Hets has been tested with zChaff 2004 11 15 11 Limits of Hets Hers is still intensively under development In particular the following points are still missing e There is no proof support for architectural specifications e Distributed libraries are always downloaded from the local disk not from the Internet e Version numbers of libraries are not considered properly e The proof engine for development graphs provides only experimental sup port for hiding links and for conservativity 12 Architecture of Hets The architecture of HETs is shown in Fig 8 How is a single logic implemented in the Heterogeneous Tool Set This is depicted in the left column of Fig 8 HEts provides an abstract interface for institutions so that new logics can be integrated smoothly In order to do so a parser a static checker and a prover for basic specifications in the logic have to be provided Each logic is realized in the programming language Haskell 30 by a set of types and functions see Fig 7 where we present a simplified stripped down version where e
16. exception is the Edit menu Moreover the nodes and links of the graph have attached pop up menus which appear when clicking with the right mouse button Edit This menu has the following submenus undo Undo the last development graph proof step see under Proofs redo Restore the last undone development graph proof step see under Proofs reload Reload the specification library Attention all proofs are lost A change management keep proofs is in preparation Unnamed nodes The Hide show names menu is a toggle you can switch on or off the display of names for nodes that are initially unnamed The newly named nodes get names that are derived from named neighbour nodes With the Hide nodes submenu it is possible to reduce the com plexity of the graph by hiding all unnamed nodes only nodes corre sponding to named specifications remain displayed Paths between named nodes going through unnamed nodes are displayed as links With the Show nodes submenu the unnamed nodes re appear 2see http www informatik uni bremen de uDrawGraph en service uDG31_doc 11 Proofs This menu allows to apply some of the deduction rules for devel opment graphs see Sect IV 4 4 of the Cast Reference Manual 28 or one of 20 21 26 While support for local and global definition or theorem links is stable support for hiding links and checking con servativity is still experimental In most cases it is advisable to use Aut
17. format is currently not used The omdoc format 14 is an XML based markup format and data model for Open Mathematical Documents It serves as semantics oriented rep resentation format and ontology language for mathematical knowledge Currently CASL specifications can be output in this format support for further logics is planned The hs format is used for Haskell modules Executable CAsL or HASCASL specifications can be translated to Haskell When the thy format is selected HeTs will try to translate each specifi cation in the library to ISABELLE and write one ISABELLE thy file per specification When the comptable xm1 format is selected HETs will extract the compo sition and inverse table of a Tarskian relation algebra from specification s selected with the n or spec option It is assumed that the relation algebra is generated by basic relations and that the specification is writ ten in the Cast logic A sample specification of a relation algebra can be found in the Hets library Calculi Space RCC8 het available from www cofi info Libraries The output format is XML the URL of the DTD is included in the XML file The pp format is for pretty printing either as plain text het AT Xinput tex or HTML html A formatter with pretty printed output currently is available only for the Cast logic For example it is possible to generate a pretty printed TFX version of Order casl by typing hets o pp tex Order casl Thi
18. g of HasCASL to Is abelle HOL 12 Haskell2IsabelleHOL coding of Haskell to Is abelle HOL 41 Haskell2IsabelleHOLCF coding of Haskell to Is abelle HOLCF 41 Modal2CASL the standard translation of modal logic to first order logic 7 PCoClTyConsHOL2IsabelleHOL coding of HasCast to Is abelle HOL SuleCFOL2SoftFOL coding of CASL to SoftFOL 17 mapping types to soft types SuleCFOL2SoftFOLIndcuction dto but with instances of induc tion axioms for all proof goals Prop2CASL inclusion Prop2CNF conversion of propositional for mulas to conjunctive normal form 4 Getting started The latest HETS version can be obtained from the HETs tools home page http www dfki de sks hets Since HETs is being improved constantly it is recommended always to use the latest version Hers currently is available for Linux Solaris and Mac OS X There are three possibilities to install HETs 1 The Java based HETs installer Download a jar file and start it with java jar file jar Note that you need Sun Java 1 4 2 or later On a Mac you can just double click on the jar file The installer will lead you through the installation with a graphical inter face It will download and install further software if not already installed on your computer CASL lib specification library http www cofi info Libraries uDraw Graph graph drawing http
19. he development graph in a GUI window Here is a summary of the types of nodes and links occurring in development graphs Named nodes correspond to a named specification Unnamed nodes correspond to an anonymous specification Elliptic nodes correspond to a specification in the current library Rectangular nodes are external nodes corresponding to a specification down loaded from another library Red nodes have open proof obligations Green nodes have all proof obligations resolved 10 Black links correspond to reference to other specifications definition links in the sense of 28 IV 4 Blue links correspond to hiding hiding definition links Red links correspond to open proof obligations theorem links Green links correspond to proved proof obligations theorem links Yellow links correspond to open proof obligations involving hiding hiding theorem links Solid links correspond to global definition or theorem links in the sense of 28 IV 4 Dashed links correspond to local definition or theorem links in the sense of 28 IV 4 Single links have homogeneous signature morphisms staying within one and the same logic Double links have heterogeneous signature morphisms moving between log ics We now explain the menus of the development graph window Most of the pull down menus of the window are uDraw Graph specific layout menus their function can be looked up in the uDraw Graph documentation The
20. ill Mossakowski Relating CAsL with other specification languages the institution level Theoretical Computer Science 286 367 475 2002 Till Mossakowski Kolyang and Bernd Krieg Brtickner Static semantic analysis and theorem proving for CASL In F Parisi Presicce editor Recent Trends in Algebraic Development Techniques 12th International Work shop WADT 97 Tarquinia Italy 1997 Selected Papers LNCS Vol 1376 pages 333 348 Springer 1998 Till Mossakowski Christian Maeder and Klaus Liittich The Heteroge neous Tool Set In Orna Grumberg and Michael Huth editors TACAS 2007 volume 4424 of Lecture Notes in Computer Science pages 519 522 Springer Verlag Heidelberg 2007 Till Mossakowski Christian Maeder and Klaus Liittich The Heteroge neous Tool Set In Bernhard Beckert editor VERIFY 2007 volume 259 of CEUR Workshop Proceedings 2007 Till Mossakowski Lutz Schr der Markus Roggenbach and Horst Reichel Algebraic co algebraic specification in CoCASL Journal of Logic and Al gebraic Programming To appear Peter D Mosses editor Cast Reference Manual volume 2960 of Lecture Notes in Computer Science Springer 2004 Free online version available at http www cofi info T Nipkow L C Paulson and M Wenzel Isabelle HOL A Proof As sistant for Higher Order Logic Springer Verlag 2002 26 30 31 32 33 34 35 36 37 38 39 40 41 42 43 S Peyton
21. l prover is launched This is described in more detail in the paragraphs below By pressing the Show Proof Details button a window is opened where for each proved goal the used axioms its proof script and its proof are shown the level of detail depends on the used theorem prover The Status shows either No prover running or Waiting for prover in black or blue If you press the Close button the window is closed and the status of the goals list is integrated into the development graph If all goals have been proved the selected node turns from red into green The list Pick Theorem Prover lets you choose one of the connected provers currently these are ISABELLE MathServe Broker Spass Vampire and zChaff described below By pressing Prove the selected prover is launched and the theory along with the selected goals is translated via the shortest possible path of comorphisms into the provers logic The button More fine grained selection lets you pick a composed comorphism in a separate window from where the prover is launched then Since the amount and kind of sentences sent to an ATP system is a major factor for the performance of the ATP system it is possible to select the axioms and proven theorems that will comprise the theory of the next proof attempt Based on this selection the sublogic may vary and also the available provers and comorphisms to provers Former theorems that are impo
22. layed Taxonomy graphs Only available for some logics Shows the subsort graph of the signature of the node Show sublogic Shows the logic and within that logic the minimal sublogic for the signature and the axioms of the node Show origin Shows the kind of Cas structuring construct that led to the node Show proof status Show open and proven local proof goals Prove Try to prove the local proof goals See Section 10 for details Check consistency Check the consistency of the theory of the node Show just subtree Only for named nodes Reduce the complexity of the graph by just showing the subtree below the current node 12 Undo show just subtree Only for named nodes Undo the reduction Show referenced library Only for external nodes Open a new win dow showing the development graph for the library the external node refers to Show number of node Show the internal number of the node Pop up menu for links Again the number of submenus depends on the type of the link Show morphism Shows the signature morphism of the link It consists of two components a logic translation and a signature morphism in the target logic of the logic translation In the most frequent case of an intra logic signature morphism the logic translation component is just the identity Show origin Shows the kind of CAs structuring construct that led to the link Show proof status Only for theorem links Show the proof status Check conser
23. n the subsort embeddings are analyzed colimit thinness perform colimit thinness check implies sharing The colimit thinness check is less complete and usually takes longer than the full cell condition check cell option but may prove more effi cient in case of certain specifications If ANALYSIS is empty then amalgamability analysis for CAsL is skipped The default value for casl amalg is cell 6 Heterogeneous Specification HEtTs accepts plain text input files with the following endings Ending default logic structuring language casl CASL CASL het CASL CASL hs Haskell Haskell owl OWL DL OWL Lite OWL Although the endings casl and het are interchangeable the former should be used for libraries of homogeneous CASL specifications and the latter for HetCast libraries of heterogeneous specifications that use the Cast struc turing constructs Within a HETCast library the current logic can be changed e g to HasCas in the following way logic HasCASL The subsequent specifications are then parsed and analysed as HAsCAsL specifications Within such specifications it is possible to use references to named CASsL specifications these are then automatically translated along the default embedding of CAsL into HAsCast cf Fig 2 There are also hetero geneous constructs for explicit translations between logics see 18 The ending hs is available for directly reading in Haskell programs and
24. o it SoftFOL 17 offers three automated theorem proving ATP systems for first order logic with equality 1 Spass 43 2 Vampire 32 and 3 Math Serve Broker 44 These together comprise some of the most advanced theorem provers for first order logic ISABELLE 29 is an interactive theorem prover for higher order logic Propositional SoftFOL and ISABELLE are currently the only logics coming with a prover Proof support for the other logics can be obtained by using logic translations to a prover supported logic An introduction to CAsL can be found in the Cast User Manual 6 the detailed language reference is given in the Cast Reference Manual 28 These documents explain both the Cast logic and language of basic specifications as well as the logic independent constructs for structured and architectural specifications The corresponding document explaining the HETCAsL language constructs for heterogeneous structured specifications is the HETCASL language summary 18 a formal semantics as well as a user manual with more exam ples are in preparation Some of HETCASL s heterogeneous constructs will be illustrated in Sect 6 below 1which chooses an appropriate ATP upon a classification of the FOL problem Propositional Prop Figure 4 Graph of most important sublogics currently supported by HETs together with their comorphisms 3 Logic translations supported by Hets Logic translations formali
25. omatic which automatically applies the rules in the correct or der As a result the the open theorem links marked in red will be reduced to local proof goals that is they become green and instead some of the node will get red indicating open local proof goals Be sides the deduction rules the menu contains entries for computing a colimit approximation for the development graph and for computing normal forms of all nodes needed when dealing with hiding Translate Graph translates the whole development graph along a logic comorphism Show Logic Graph shows the graph of logics and logic comorphisms currently supported by HETS Show Library Graph shows the graph of libraries that have been loaded into HETS and their dependencies For library the corresponding de velopment graphs can be shown using its node menu Also a list of specifications and views can be shown Pop up menu for nodes Here the number of submenus depends on the type of the node Show signature Shows the signature of the node Show local axioms Shows the local axioms of the node Show theory Shows the theory of the node including axioms imported from other nodes Warning axioms imported via hiding links are not part of the theory they can be made visible only by re adding the hidden symbols using the proof rule Theorem Hide Shift Translate theory Translates the theory of a node to another logic A menu with the possible translation paths will be disp
26. on of proof obligations z Management of proofs amp change Grothendieck logic Flattened logic graph Heterogeneous proof trees Conservativity and Model checkers Figure 8 Architecture of the heterogeneous tool set The static analysis is based on the static analysis of basic specifications and transforms an abstract syntax tree to a development graph cf Sect 7 above Starting with a node corresponding to the empty theory it successively extends using the static analysis of basic specifications and or translates along the intra and inter logic translations the theory while simultaneously adding nodes and links to the development graph Heterogeneous proof management is done using heterogeneous development graphs as described in Sect 7 For local proof goals logic specific provers are invoked see Sect 10 HETs can store development graphs including their proofs Therefore HETS uses the so called ATerm format 8 which is used as interchange format for interfacing with other tools More details can be found in 20 26 and in the overview of modules provided in the developers section of the HETs home page at http www dfki de sks hets Hers is mainly maintained by Christian Maeder Christian Maeder dfki de and Till Mossakowski Till Mossakowski dfki de The mailing list is hets users informatik uni bremen de the homepage is 23 http www informatik uni bremen de mailman listinfo hets users You nee
27. ping into some shell hets Order casl Hers checks both the correctness of this specification with respect to the CAsL syntax as well as its correctness with respect to the static semantics e g whether all identifiers have been declared before they are used whether opera tors are applied to arguments of the correct sorts whether the use of overloaded symbols is unambiguous and so on The following flags are available in this context p just parse Just do the parsing the static analysis is skipped s just structured Do the parsing and the static analysis of heteroge neous structured specifications but leave out the analysis of basic spec ifications This can be used for prototyping issues namely to quickly produce a development graph showing the dependencies among the spec ifications cf Sect 7 even if the individual specifications are not correct yet L DIR hets libdir DIR Use DIR as the directory for specification libraries equivalently you can set the variable HETS_LIB before calling Hers casl amalg ANALYSIS For the analysis of architectural specification a quite advanced feature of CAsL the ANALYSIS argument specifies the options for amalgamability checking algorithm for Cast logic it is a comma separated list of zero or more of the following options sharing perform sharing analysis for sorts operations and predicates cell perform cell condition check implies sharing With this option o
28. qual ity clauses 4 The list of problem classes for each ATP system is not exhaustive but only the most appropriate problem classes are named according to benchmark tests made with MathServe by Jiirgen Zimmer Table 1 ATP systems provided as Web services by MathServe of the Web services provided by the MathServe system are used by HETS cur rently Vampire and the brokering system The ATP systems are offered as Web Services using standardized protocols and formats such as SOAP HTTP and XML Currently the ATP system Vampire may be accessed from HETs via MathServe the other systems are only reached after brokering SPASS The ATP system Spass 43 is a resolution based prover for first order logic with equality Furthermore it provides a soft typing mechanism with subsorting that treats sorts as unary predicates The ATP Spass should be installed locally and available through your PATH environment variable Vampire The ATP system Vampire is the winner of the last 5 CADE ATP System Com petitions CASC 2002 2006 in the devisions FOF and CNF It is a resolution based ATP system supporting the calculi of ordered binary resolution and super position for handling equality See http www cs miami edu tptp CASC J3 SystemDescriptions html Vampire 8 0 for detailed information The connection to Vampire is achieved by using an Web service of the MathServe system MathServe Broker The brokering service chooses
29. r structured and architectural specifications and libraries The latter of course needs to call the logic specific tools whenever a basic specification is encountered Hers is based on the theory of institutions 11 which formalize the notion of a logic The theory behind Hers is laid out in 20 A short overview of HETS is given in 25 26 SPEC BASIC SPEC SPEC then SPEC SPEC then implies SPEC SPEC with SYMBOL MAP SPEC with logic ID DEFINITION logic ID spec ID SPEC end view ID SPEC to SPEC SYMBOL MAP end view ID SPEC to SPEC with logic ID end LIBRARY DEFINITION Figure 1 Syntax of a simple subset of the heterogeneous specification language BASIC SPEC and SYMBOL MAP have a logic specific syntax while ID stands for some form of identifiers 2 Logics supported by Hets The following list of logics formalized as so called institutions 11 is currently supported by HETS CASL extends many sorted first order logic with partial functions and subsort ing It also provides induction sentences expressing the free generation of datatypes For more details on Cas see 28 6 We have implemented the Cast logic in such a way that much of the implementation can be re used for Cast extensions as well this is achieved via holes realized via polymorphic variables in the types for signatures morphisms abstract syntax etc This eases integration of CASL extensions and keeps th
30. rted from other specifications are marked with the prefix Th Since former theorems do not add additional logical content they may be safely removed from the theory 10 1 Automated Theorem Proving Systems Logic SoftFOL All ATPs integrated into HETs share the same GUI with only a slight modifi cation for the MathServe Broker it does not have input fields for extra options Figure 6 shows the instantiation for SPAss where in the lower part of the win dow the batch mode can be controlled The upper part shows on the left the list of goals with the same status indicators as in the Proof Management GUI and on the right a proof attempt of the selected goal is controlled and the re sult of the last proof attempt is displayed The status line indicates Open Running Proved Disproved Open Time is up and Proved Theory inconsistent The list of used axioms is actually only filled by Spass The help button displays information about the extra options accepted by the ATP system The button Show Details shows the whole output of the ATP system Save Prover Configuration allows you to save the configuration and status of each proof for documentation By pressing the button Exit Prover the status of these proofs and goals is transferred back to the Proof Management GUI The MathServe system 44 developed by Jiirgen Zimmer provides a unified interface to a range of different ATP system
31. s the most important systems are listed in Table 1 along with their capabilities These capabilities are derived from the Specialist Problem Classes SPCs defined upon the basis of logical language and syntactical properties by Sutcliffe and Suttner 38 Only two 17 O Calculi Space RCCVerification_ExtRCCByRCC5Rels_E1 SPASS Prover Goals g Options T J sym DR TimeLimit 10 sym_PO sym_EQ disj_DR disj_PO disj_PP disj_PPi disj_EQ cmps_PPPP cmps_PPPPi cmps_PPPO cmps_PPDR cmps_PPEQ cmps_PPiPP cmps_PPiPPi cmps_PPiPO Extra Options Results h Status Proved l Options TimeLimit Extra Options Current goal Global Options v include preceeding proven therorems in next proof attempt Save Prover Configuration A Figure 6 Interface of the SPAss prover 18 ATP System Version Suitable Problem Classes DCTP 10 21p effectively propositional EP 0 91 effectively propositional real first order no equality real first order equality Otter 3 3 real first order no equality SPASS 2 2 effectively propositional real first order no equality real first order equality Vampire 8 0 effectively propositional pure equality equal ity clauses contain non unit equality clauses real first order no equality non Horn Waldmeister 704 pure equality equality clauses are unit e
32. s will generate a file Order pp tex It can be included into ATRX documents provided that the style hetcasl sty coming with the HETS distribution LaTeX hetcasl sty is used The dfg format is used by the Spass theorem prover 43 14 The tptp format http www tptp org is a standard format for first order theorem provers t TRANS translation TRANS chooses a translation option TRANS is a colon separated list without blanks of one or more comorphism names see Sect 3 R recursive output also imported libraries The other output formats are for future usage 9 Miscellaneous Options v Int verbose Int Set the verbosity level according to Int Default is 1 q quiet Be quiet no diagnostic output at all Overrides v V version Print version number and exit h help usage Print usage information and exit RTS KIntM RTS Increase the stack size to Int megabytes needed in case of a stack overflow This must be the first option 1 LOGIC logic LOGIC chooses the initial logic which is used for processing the specifications before the first logic L declaration The default is Cast n SPECS spec SPECS chooses a list of named specifications for processing m FILE modelSparQ FILE model check a qualitative calculus given in SparQ lisp notation 42 against a Cast specification I interactive run HETs in interactive mode 10 Proofs with Hers The proof calculus for developmen
33. s with ISABELLE will not conform to the syntax of the original input logic They may even use features of ISABELLE HoL such as higher order functions that are not present in an input logic like Cast ISABELLE is started with ProofGeneral 2 1 in a separate Emacs 9 40 The ISABELLE theory file conforms to the Isabelle Isar syntax 29 It starts with the theory encoded along the selected comorphism followed by a list of theorems Initially all the theorems have trivial proofs using the oops command However if you have saved earlier proof attempts HETs will patch these into the generated ISABELLE theory file ensuring that your previous work is not lost But note that this patching can only be successful if you do not rename specifications or change their structure You now can replace the oops commands with real ISABELLE proofs and use Proof General to step through the proofs You finish your session by saving your file using the Emacs file menu or the Ctrl x Ctrl s key sequence and by exiting Emacs Ctrl x Ctrl c 10 3 zChaff zChaff is a solver for satisfiabily problems of boolean formulas SAT in CNF It is connected as a prover for propositional logic to Hers The prover Spass is used to transform arbitrary boolean formulas to CNF zChaff implements the CHAFF algorithm We are using the property that a conjecture under the assumption of a set of axioms is true if the variables of axioms togeth
34. t graphs Sect 7 reduces global theorem links to local proof goals Local proof goals indicated by red nodes in the development graph can be eventually discharged using a theorem prover using the Prove menu of a red node The graphical user interface GUI for calling a prover is shown in Fig 5 we call it Proof Management GUI The list on the left shows all goal names prefixed with the proof status in square brackets A proved goal is indicated by a a indicates a disproved goal a space denotes an open goal and a x denotes an inconsistent specification aka a fallen see below for details If you open this GUI when processing the goals of one node for the first time it will show all goals as open Within this list you can select those goals that should be inspected or proved The button Display shows the selected 15 Saad Goal s Display Prove Show proof details Status No Prover Running Sublogic of Currently Selected Theory CASL SulFOL Pick Theorem Prover abelle athServe Broker Select open goals More fine grained selection Fine grained composition of theory Axioms to include Theorems to include if proven Deselect former theorems Show theory Show selected theory Close Figure 5 Hets Goal and Prover Interface NN goals in the ASCII syntax of this theory s logic in a separate window With the Prove button the actua
35. the source node including the inherited ones hold in the target node while a local theorem link only postulates that the local axioms of the source node hold in the target node Both definition and theorem links can be homogeneous i e stay within the same logic or heterogeneous i e the logic changes along the arrow Technically this is the case for Grothendieck signature morphisms p o where p 4 id This case is indicated with double arrows Theorem links are initially displayed in red The proof calculus for develop ment graphs 21 20 is given by rules that allow for proving global theorem links by decomposing them into simpler local and global ones Theorem links that have been proved with this calculus are drawn in green Local theorem links can be proved by turning them into local proof goals The latter can be discharged using a logic specific calculus as given by an entailment system for a specific institution Open local proof goals are indicated by marking the corresponding node in the development graph as red if all local implications are proved the node is turned into green This implementation ultimately is based on a theo rem 20 stating soundness and relative completeness of the proof calculus for heterogeneous development graphs Details can be found in the Cast Reference Manual 28 IV 4 and in 20 21 26 The following option lets HETs show the development graph of a specification library g gui Shows t
36. vativity Experimental Check whether the theory of the target node of the link is a conservative extension of the theory of the source node Show ID of this edge Shows the internal number of the edge These numbers are also used in the proof status information for edges 8 Reading Writing and Formatting HETs provides several options controlling the types of files that are read and written i ITYPE input type ITYPE Specify ITYPE as the type of the input file The default is het HETCAst plain text ast is for reading in abstract syntax trees in ATerm format while ast baf reads in the compressed ATerm format The possible input types are casl het owl hs prf omdoc hpf tree gen_trm baf 0 DIR output dir DIR Specify DIR as destination directory for output files o OTYPES output types O0TYPES OTYPES is a comma separated list of out put types prf env omdoc hs 13 thy comptable xml sig th delta pp het tex graph exp dot dot dfg c tptp c The default is prf a synonym for dg taf which means that the devel opment graph of the library is stored in textual ATerm format taf This format can be read in when a library is downloaded from another library avoiding the need to re analyse the downloaded library You can also di rectly read in the prf format both from the command line by calling HETs on the prf file and from the GUI using the File Open menu The env
37. zed as institution comorphisms 10 translate from a given source logic to a given target logic More precisely one and the same logic translation may have several source and target sublogics for each source sublogic the corresponding sublogic of the target logic is indicated A graph of the most important logics and sublogics together with their comorphisms is shown in Fig 4 In more detail the following list of logic translations is currently supported by HETS CASL2CoCASL inclusion CASL2CspCASL inclusion CASL2HasCASL inclusion CASL2Modal inclusion CASL2PCFOL coding of subsorting by injec tions see Chap III 3 1 of the CASL Reference Manual 28 CASL2SubCFOL coding of partial functions by er ror elements translation 4a of 23 but extended to subsorting CASL2TopSort coding of subsorting by a top sort and unary predicates for the sub sorts CFOL2IsabelleHOL coding of Cast to Isabelle trans lation 7 of 23 CoCASL2CoPCFOL coding of subsorting by injec tions similar to CASL2PCFOL CoCASL2CoSubCFOL coding of partial functions by error supersorts similar to CASL2SubCFOL CoCFOL2IsabelleHOL coding of CoCast to Isabelle similar to CFOL2IsabelleHOL HasCASL2HasCASL coding of HASCASL axiomatic re cursive definitions as HasCasi recursive program definitions HasCASL2Haskell translation of HASCASL recursive program definitions to Haskell HasCASL2IsabelleHOL codin
Download Pdf Manuals
Related Search