Hets for Common Logic Users
Contents
1. emps NIPPDC ee PIT r arar ya cmps_ECEC Save dfg File Show Details Help Save config Close Figure 10 Interface of the Spass prover 22 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 Furthermore 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 IsaseLLE 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 Hox logic is different from the logics that are encoded into it via comorphisms Therefore the formulas appearing in subgoals of proofs 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 in a separate Emacs 43 The Isasette theory file con forms to the Isabell2. 2 2 OWL2 OWL2 is a WSC standard 3 Hers can directly read in OWL2 files in all syntaxes called serialisa tions that the OWL API supports 2 including the native OWL XML syntax 31 the human readable Manchester syntax 21 as well as RDF 35 The RDF data model has multiple possible syntaxes itself including RDF XML 7 and the text oriented Turtle syntax 8 Since OWL2 does not support relative theory interpretations and other structuring features such things can only be expressed in HetCast files For this purpose OWL2 Manchester syntax can be used within HetCast files or OWL2 files can be referred to within HerCasu files 2 3 HetCASL For heterogeneous specification Herts offers the Heterogeneous language HetTCas HETCasi is not so much a logic but a meta language that can express relations of theories written in different logics like logical consequences relative interpretations of theories conservative extensions translations of theories along logic translations etc HetCasi generalises the structuring constructs of Cas Common Algebraic Specification Language 29 to arbitrary logics if they are formalised as institutions and plugged into the Hers motherboard as well as to heterogeneous combinations of specifications written in different logics See Fig 1 for a simple subset of the HerCas syntax where basic specifications are unstructured specifications or modules written in a specific logic The graph
3. Include preceding proven theorems in next proof attempt _ Save problem batch Stop Prove Results Status Proved Used Axioms Save tptp File I Show Details Save config Close SS Figure 6 Interface of Vampire Prover 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 GUI elements are the following e The button Display shows the selected goals in the ASCII syntax of this theory s logic in a separate window e By pressing the 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 18 Prove all e With the Prove button the actual prover is launched The provers are described in more detail in the Hers user guide 44 e The list Pick Theorem Prover lets you choose one of the connected provers among them 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 prover s logic e The pop up choice box below Selected comorphism path lets you pick a composed comorphism to be used for the chosen prover If
4. Snow Leopard we provide a meta package Hets mpkg based on MacPorts that will be extended by further tools for proving in the future 3 Then we have Java based Herts installer that we may drop in the future Download a jar file and start it with java jar file jar Note that you need Sun Oracle Java 1 4 2 or later On a Mac you can just double click on the jar file but you have to install the MacPorts 1ibglade2 package and all its dependencies yourself In order to speed this up we provide a meta package 1ibglade2 mpkg too The installer will lead you through the installation with a graphical interface It will download and install further software if not already installed on your computer Hets lib specification library http www cofi info Libraries ss uDraw Graph graph drawing http www informatik uni bremen de uDrawGraph en Tel Tk graphics widget system version 8 4 or 8 5 must be installed before Spass theorem prover attp spass mpi sb mpg de Darwin theorem prover should be installed manually from http combination cs uiowa edu Darwin ISABELLE theorem prover http www cl cam ac uk Research HVG Isabelle editor for Isabelle must be installed manually 4 If you do not have Sun Oracle Java you can just download the hets binary You have to unpack it with bunzip2 and then put it into some place covered by your PATH environment variable You also have to install the ab
5. of currently supported logics and logic translations the latter are also called comorphisms is shown in Fig 2 and the degree of support by Hers in Fig 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 Specification libraries are collections of named structured and architectural specifi cations Refinements express the fact the a specification is becoming more specific All this is supported by HetCast For details see 29 3 Logics supported by Hets Herts supports a variety of different logics The following are most important for use with Common Logic Common Logic is an ISO standard published as ISO IEC 24707 2007 Information technology Com mon Logic CL a framework for a family of logic based languages 12 It is based on first order Listing 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 SPEC 71 BASLIC SPEC 3 logic specific syntax e g CLIF or Manchester syntax SPEC then SPEC SPEC then implies SPEC SPEC with SYMBOL MAP SPEC with logic ID o o o o extension of a spec with new symbols and axioms annotation extension is logically implied renaming of SPEC along SYMBOL MAP translation of SPEC
6. perform induc tion proofs in theories involving sequence markers e aconnection to first order model finders like darwin that allow one to find models for CL theories e support for proving interpretations between CL theories to be correct e a translation that eliminates the use of CL modules Since the semantics of CL modules is special to CL this elimination of modules is necessary before sending CL theories to a standard first order prover e a translation of the Web Ontology Language OWL to CL e a translation of propositional logic to CL This guide will introduce you to these functionalities of Hers For the full functionalities of HEts see the Herts user guide 44 2 The Heterogeneous Tool Set and Its Input Languages The central idea of the Heterogeneous Tool Set Hers is to provide a general framework for formal methods integration and proof management One can think of Hers acting like a motherboard where different expansion cards can be plugged in the expansion cards here being individual logics with their analysis and proof tools as well as logic translations The Hers motherboard already has plugged in a number of expansion cards e g the theorem provers Isabelle SPASS and more as well as model finders Hence a variety of tools is available without the need to hard wire each tool to the logic at hand Hets consists of logic specific tools for the parsing and static analysis of the different involved logics as wel
7. to a different logic oo oo oo oo alo ole DEFINITION logic ID select a new logic for subsequent items spec ID SPEC end give the name ID to SPEC view ID SPEC to SPEC SYMBOL MAP end interpretation of theories view ID SPEC to SPEC logic ID end oo dto but across different logics LIBRARY DEFINITION gt inclusion subinstitution model expansive comorphism gt faithful comorphism th theoroidal comorphism inf comorphism generating infinite signatures red full higher order logic orange some second order constructs yellow semi decidable first order logic green decidable ontology language Figure 2 Graph of logics related to Common Logic that are currently supported by HEts logic but extends first order logic in several ways The Common Logic Interchange Format CLIF provides a Lisp like syntax for Common Logic Herts currently only supports parsing CLIF If you need other dialects send us a message and we will add them OWL2 is the Web Ontology Language recommended by the World Wide Web Consortium W3C www w3c org see 3 It is used for knowledge representation on the Semantic Web 10 Hets calls an external OWL2 parser written in Java to obtain the abstract syntax for an OWL file and its imports The Java parser also does a first analysis classifying the OWL ontology into the sublanguages OWL Full all of OWL under the RDF semantics u
8. will create files for consistency checks by SPASS or Darwin respec tively For all output formats it is recommended to increase the verbosity to at least level 2 by using the option v2 to get feedback which files are actually written v2 also shows which files are read t TRANS translation TRANS chooses a translation option TRANS is a colon separated list without blanks of one or more comorphism names see Sect 4 n SPECS spec SPECS chooses a list of named specifications for processing w NVIEWS view NVIEWS chooses a list of named views for processing R recursive output also imported libraries I interactive run Herts in interactive mode X server run Herts as web server see Sect 11 x xml use XML PGIF packets to communicate with Hers in interactive mode S PORT listen PORT communicate with Herts in interactive mode by listening to the port PORT c HOSTNAME PORT connect HOSTNAME PORT communicate with Herts in interactive mode via connecting to the port on host HOSTNAME d STRING dump STRING produces implementation dependent output for debugging purposes only i e d LogicGraph lists the logics and comorphisms 11 Hets as a web server Large parts of Hets are now also available via a web interface A running server should be accessible on p pollux informatik uni bremen de 8000 It allows to browse the Herts library upload a file or just a HETCasi specification Development graphs
9. x y x K The heterogeneous library CommonLogic Examples SymbolMap het in the Hers library es tablishes a mapping actually a relative interpretation between these two Common Logic texts library SymbolMap logic CommonLogic from upper get upper from lower get lower view v lower with a gt A b gt B to upper view w upper with A gt a B gt b to lower A symbol map only needs to list those names that differ between the source and the target ontology the other names none in this concrete case are implicitly the same A mapping of a single name is defined with nameInTargetFile gt nameInCurrentFile multiple mappings are separated by commas Note that in Common Logic a comma can be part of a name Hence a space must be placed between the separation comma and a name 8While the copy semantics of Common Logic importations does not permit renamings HETCASL s extension mechanism offers an alternative possibility to reuse ontologies and rename some of their symbols using the importedSpec with name1Old gt name1New name2Old gt name2New then importingSpec syntax 12 BoundedLattice n Figure 3 Boolean algebras and lattices in COLORE subgraph 8 2 2 Relative Interpretation in COLORE We give two examples for relative interpretation one from COLORE in this section and one standalone one in Sect 8 2 3 The COLORE module RegionBooleanContactAlgebra relat
10. 10 2009 Bjorn Pelzer and Christoph Wernhard System description E krhyper In Frank Pfenning editor CADE volume 4603 of Lecture Notes in Computer Science pages 508 513 Springer 2007 Alexandre Riazanov and Andrei Voronkov The design and implementation of VAMPIRE AI Com munications 15 2 3 91 110 2002 Michael Schneider OWL 2 web ontology language RDF based semantics W3C recommendation World Wide Web Consortium W3C October 2009 W Marco Schorlemmer and Yannis Kalfoglou Institutionalising ontology based semantic integra tion Applied Ontology 3 3 131 150 2008 S Schulz E A Brainiac Theorem Prover Journal of AI Communications 15 2 3 111 126 2002 Geoff Sutcliffe The TPTP world infrastructure for automated reasoning In Edmund M Clarke and Andrei Voronkov editors LPAR Dakar volume 6355 of Lecture Notes in Computer Science pages 1 12 Springer 2010 Geoff Sutcliffe and Christian B Suttner Evaluating general purpose automated theorem proving systems Artificial Intelligence 131 1 2 39 54 2001 http www xemacs org People index html XEmacs Available at http www Mihai Codescu Till Mossakowski Christian Maeder Hets user guide 2011 www informatik uni bremen de agbkb forschung formal_methods CoFI hets UserGuide pdf 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 Hillenbr
11. Hets for Common Logic Users Version 0 99 Till Mossakowski Christian Maeder Mihai Codescu Eugen Kuksa Christoph Lange DFKI GmbH Bremen Germany Comments to hets users informatik uni bremen de the latter needs subscription to the mailing list 10th January 2013 Contents 1 2 3 6 6 7 8 9 17 10 Reading Writing and Formatting 23 25 25 1 Introduction Common Logic CL is an ISO standard published as ISO IEC 24707 2007 Information technology Common Logic CL a framework for a family of logic based languages 12 CL is based on untyped first order logic but extends first order logic in two ways 1 any term can be used as function or predicate and 2 sequence markers allow for talking about sequences of individuals directly The Heterogeneous Tool Set Hers is an open source software providing several kinds of tool support for Common Logic Strictly speaking only the second feature goes beyond first order logic Hets motherboard isabelle 1 SPASS a M atl QEVE kn P S Ti pe Figure 1 The Hers motherboard and some expansion cards e a parser for the Common Logic Interchange Format CLIF CLIF is a Lisp like syntax for CL e aconnection of CL to well known first order theorem provers like SPASS darwin and Vampire such that logical consequences of CL theories can be proved e a connection of CL to the higher order provers Isabelle HOL and Leo II in order to
12. Riichiro Mizoguchi editors Formal Ontology in Information Systems Proceedings of the Sixth International Conference FOIS 2010 number 209 in Frontiers in Artificial Intelligence and Applications pages 317 330 IOS Press 2010 Marc Herbstritt zChaff Modifications and extensions report00188 Institut fiir Informatik Uni versitat Freiburg July 17 2003 Thu 17 Jul 2003 17 11 37 GET Matthew Horridge and Peter F Patel Schneider OWL 2 web ontology language Manchester syntax W3C candidate recommendation World Wide Web Consortium W3C 10 2009 Michael Kohlhase OMDoc An Open Markup Format for Mathematical Documents version 1 2 volume 4180 of Lecture Notes in Computer Science Springer 2006 Klaus L ttich and Till Mossakowski Reasoning Support for CASL with Automated Theorem Proving Systems In J Fiadeiro editor WADT 2006 number 4409 in LNCS pages 74 91 Springer 2007 T Mossakowski HetCASL heterogeneous specification Language 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 Christian Maeder and Klaus Luttich The Heterogeneous Tool Set In Orna Grumberg and Michael Huth editors TACAS 2007 volume 4424 of Lecture Notes i
13. WLandCL het in the Hers library 1 establishes a view between the OWL Time ontology and its reimplementation in Common Logic using the OWL22CommonLogic translation logic OWL spec TimeOWL Class TemporalEntity ObjectProperty before Domain TemporalEntity Range TemporalkEntity Characteristics Transitive end logic CommonLogic spec TimeCL 6 CommonLogic equivalent of Domain and Range above forall tl t2 L before t1 t2 and TemporalEntity t1 TemporalEntity t2 6 CommonLogic equivalent of Transitive above forall t1 t2 t3 1 and before tl t2 before t2 t3 before tl t3 A new axiom that cannot be expressed in OWL forall tl t2 or before tl t2 before t2 t1 TL 22 o o end view TimeOWLtoCL TimeOWL with logic OWL22CommonLogic to TimeCL As OWL22CommonLogic is the default translation it is optional to specify it oo ole o G Q oO 9 Proofs with Hers The proof calculus for development graphs Sect 8 reduces global theorem links to local proof goals You can do this reduction by clicking on the Edit menu in the development graph window and selecting Proofs Auto DG Prover Local proof goals indicated by red nodes in the development graph can be eventually discharged using a theorem prover i e by 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 Man agement GUI T
14. alizing a first order spatial calculus e In particular the compact representation of mutual disjointness chosen here makes use of Common Logic s sequence markers e As Common Logic module extends the previously imported OWL ontology it has access to all enti ties of the OWL ontology by name in particular we can specify that two rooms are connected in terms of the OpenAAL terminology if certain conditions in terms of our Common Logic module or certain conditions in terms of OpenAAL hold Ahnttp openaal org 15 library AAL logic OWL from OpenAALOntology get httpwwwdfkideskshetsontologyunnamed gt OpenAAL this is the default name that Hets assigns to unnamed ontologies but we rename it to something nicer oo lo oo ole spec OurAAL 3 Import the OpenAAL OWL ontology OpenAAL some other extensions not shown here Extend it by an RCC style spatial calculus formalized in first order logic then logic CommonLogic forall al a2 or equal al a2 overlapping al a2 bordering al a2 disconnected al a2 oproper_part_of al a2 oproper_part_of a2 al mutual disjointness of predicates need this for an exclusive or forall p MUL Wal by O 1S O7Te P7 forall pg iff ite lis dISJOrnt P Q tay and forall x not and p X q X mutua tlry drisJornt E sers m t aliv dIs Jornet GF ns IN a utility predicate for talking about inverse relations similar to owl inverseOf for
15. all r x y 1f converse r x y yY X make the above or exclusive mutually disjoint egual overlapping bordering disconnected proper_part_of converse proper_part_of if some RCC relations hold so far it would also work in OWL or if there is a door that connects two rooms then the latter would only work in OWL if we used an explicit subproperty is door of of is in room then we could chain inverse is door of and is door of but otherwise we wouldn t be able to restrict the connecting element to a Door forall al a2 if or equal al a2 overlapping al a2 proper_part_of al a2 oo o ob oO oP o oo o o op alo o proper_part_of a2 al exists door and Door door is in room door al is in room door a2 is connected to room al a2 16 8 2 5 Heterogeneous Views from OWL to Common Logic In the previous example we established a link between an OWL ontology and a Common Logic ontol ogy by reusing elements of the signature of the OWL ontology concretely OpenAAL s is in room predicate in the Common Logic ontology HetCas s view mechanism offers an alternative to that A view from one ontology to another ontology in the same logic has been shown in Sect 8 2 2 but it is also possible to have views across logics as long as there is a translation between these logics that is known to Herts cf Sect 4 The following example which is available as Ontology Examples TimeInO
16. and 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 Jurgen Zimmer and Serge Autexier The MathServe System for Semantic Web Reasoning Services In U Furbach and N Shankar editors 3rd IJCAR LNCS 4130 Springer 2006 28
17. ation Proving SZS status SatisFiable For tmp cat_cat9010 tptp MODEL TPTP SZS output start FiniteModel For tmp cat_cat9010 tptp FoF interpretation_domain Fi_domain x X e1 FoF interpretation_atoms Fi_predicates X0 X1 attr_2 X0 X1 y x0 cat_1 X0 i XO happy_1 X0 i X0 X1 on_2 X0 X1 lt gt Ffalse i x0 p_1 X0 amp XO pet_1 X0 amp lt gt Close Figure 9 Consistency checker results _ATP System Suitable Problem Classes a 10 21p effectively propositional gt propositional effectively propositional real first order no equality real first order equality real first order no equality ald pee propositional real first order no all real first order equality Vampire effectively propositional pure equality equal ity clauses contain non unit equality clauses po real first order no equality non Horn Waldmeister pure equality equality clauses are unit equal a The list of problem classes for each ATP system is not exhaustive but only the most ap propriate problem classes are named according to benchmark tests made with MathServe by Jurgen Zimmer Table 1 ATP systems provided as Web services by MathServe These capabilities are derived from the Specialist Problem Classes SPCs defined upon the basis of logical language and syntactical properties by Sutcliffe and Suttner 42 Only two of the W
18. bligations 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 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 heteroge neous i e the logic changes along the arrow Theorem links are initially displayed in red The proof calculus for development graphs 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 by Hers 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 theorem stating soundness and relative completeness of the proof calculus for heterogeneous development graphs Details can be found in the Cast Reference Manual IV 4 and in 28 The following options let Hers display the development graph of a specification libra
19. c CommonLogic The subsequent specifications are then parsed and analysed as Common Logic specifications Within such specifications it is possible to use references to named Casi specifications these are then automat ically translated along the default embedding of Cas into Common Logic cf Fig 2 There are also heterogeneous constructs for explicit translations between logics see The endings clf and clif are available for directly reading in Common Logic CLIF texts as in the example of Cat AllInOne clif By contrast in HerCasi libraries ending with het the logic Common Logic has to be chosen explicitly and the Cas structuring syntax needs to be used library Cat logic CommonLogic spec Pred P x and P x Q y 4This file can be found in the CommonLogic Examples directory in the HETS library i spec Cat or Cat x Mat y not On x y if P x Q x spec PetHappy Pred and Cat then exists z and Pet x Happy z Attr x z end Note that the dot at the beginning of a line indicates that a new text begins Hence it is possible to have multiple texts in a Cas specification This specification is the HerCas structured equivalent to the following three CLIF files Pred clif cl text Pred P x and P x Q y Cat clif cl text Cat or Cat x Mat y not On x y if P x Q x Spec clif cl text PetHappy cl imports Pred cl imports Cat exists z and P
20. e Isar syntax 34 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 Herts 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 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 explicit type of the input file exp files contain a development graph in a new experimental OMDoc format prf files contain additional development steps as shared ATerms to be applied on top of an underlying develop ment graph created from a corresponding env casl or het file hpf files are plain text files representing heterogeneous proof scripts The contents of a hpf file must be valid input for Herts in interactive mode gen_trm formats are currently not supported The possible input types are casl het owl hs exp maude elf hol Pri
21. eb services provided by the MathServe system are used by Hers currently Vampire and the brokering system The ATP systems are offered as Web Services using standardised protocols and formats such as SOAP HTTP and XML Currently the ATP system Vampire may be accessed from Herts via MathServe the other systems are only reached after brokering For details on the ATPs supported see the Hers user guide 44 9 3 Interactive Theorem Proving Systems The main interative theorem proving system integrated into Hers is IsaBELLE 34 an interactive theorem prover It is more powerful than ATP systems but also requires more user interaction In particular Isabelle can be used to perform induction proofs about Common Logic theories involving sequence mark ers 21 SPASS Calculi Space RCCVerification ExtRCCByRCC8Rels_E2 A Goals Options t emps NTPPINTPPI Timeout 110 t cmps_ NTPPITPPI Extra Options it cmps_ TPP TPPi re it cmps_ TPPINTPP m Include preceeding proven t cmps_TPPINTPPI theorems in next proof attempt p O Save problem batch stop Prove Prove all cmps_DCEC Results cmps_DCNTPP a USGI loms pP_ det nT PP_def ga_non_empty sort reg pO def o impl t emps _ TPPITPP emps DCNTPPI emps DOPO emps DCTPP emps DCIPPI emps ECDC p impl O cmps ECNTPP cmps ECNTPPI emps ECPO cmos ECTPP p def c_ non triv extens PP_def emps ECTPPI
22. ecification with respect to the CLIF syntax as well as its correctness with respect to the static semantics The following flags are available in this context p just parse Just do the parsing the static analysis is skipped and no development graph is created s just structured Do the parsing and the static analysis of heterogeneous structured specifi cations but leave out the analysis of basic specifications This can be used for prototyping issues namely to quickly produce a development graph showing the dependencies among the specifica tions cf Sect 8 even if the individual specifications are not correct yet L DIR hets libdir DIR Use DIR as a colon separated list of directories for specification li braries equivalently you can set the variable HETS_LIB before calling Herts There are more flags which can be used with Hers see 44 7 Heterogeneous Specification Hets accepts plain text input files for the presented logics with the following endings default logic structuring language re o ea oo om owa OWI2 elf or clif CommonLogic custom see Sect B1 Although the endings casl and het are abit the former should be used for libraries of homogeneous Casi specifications and the latter for HerCasz libraries of heterogeneous specifications that use the Casi structuring constructs Within a HerCast library the current logic can be changed e g to Common Logic in the following way logi
23. ers User Guide 8 1 Relations between Common Logic Texts Hers supports several relations between Common Logic Texts However only one of them the impor tation is defined in ISO IEC 24707 2007 12 and has a syntax within Common Logic All the other relations are unofficial extensions used e g by the Common Logic Repository COLORE 17 and repre sented externally of Common Logic texts COLORE currently represents them in external XML documents and any required symbol maps in external CLIF files Hers in contrast allows for declaring them as views within HeTCas files outside of specifications as can be seen from the syntax specification in List Importation is defined in ISO IEC 24707 2007 as virtual copying of a resource In Hets a whole file is copied into the importing specification Hets cannot currently handle cyclic imports If you really need them send us a message at hets informatik uni bremen de and we will fix it Using CLIF you can import someFile clif via cl imports someFile clif Omitting the file extension will also succeed In this case Hers will look for a file called someFile clif in first place and then for someFile c1f in the current directory and then in the library paths Hets also supports URIs for importing resources The allowed URI schemes are file http and RECOS cl imports file absolute path to someFile clif cl imports http someDomain com path to someFile clif cl imports ht
24. et x Happy z Attr x z Both can be directly used with Hers where the former content would be in a file with the extension het and the latter in a file with one of the extensions clf or clif 6 This specification is divided into three parts which are linked to each other These links and some more information can be seen in the development graph of the file 8 Development Graphs Development graphs are a simple kernel formalism for heterogeneous structured 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 edges called definition links indicating the dependency of each involved Note that the cl text syntax specified in the Common Logic standard has subsequently been recorded as a defect T3 in favor of cl text HETS supports both These files can be found in the CommonLogic Examples directory in the HETS library T 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 Theorem links are the central data structure to represent proof o
25. fication in the library to ISABELLE and write one ISABELLE thy file per specification When the comptable xml format is selected Hers will extract the composition and inverse ta ble 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 written in the Casi logic A sample specification of a relation algebra can be found under Calculi Space RCC8 het in the Herts library 1 The output format is XML the URL of the DTD is included in the XML file The sig or th option will create HETCas signature or theory files for each development graph node The delta extension is not yet supported The pp format is for pretty printing either as plain text het BIFX input tex HTML htm1 or XML xml For example it is possible to generate a pretty printed BIFX version of Cat clif by typing hets vzZ O ppwtex Catb clir This will generate a file Cat pp tex It can be included into AleX documents provided that the style hetcasl sty coming with the Hets distribution LaTeX hetcasl sty is used The format pp xm1 represents just a parsed library in XML 24 Formats with graph are reserved for future usage The dfg format is used by the Spass theorem prover 46 The tptp format http www tptp org is a standard exchange format for first order theorem provers Appending c to dfg or tptp
26. for well formed specifications can be displayed in various formats where the svg format is supposed to look like the graphs displayed by uDrawGraph Besides browsing the web server is supposed to be accessed by other programs using queries The possible queries are described athttp trac informatik uni bremen de 8080 hets wiki For details on this topic see the Hers user guide 44 12 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 11Proof General Interface Protocol 23 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 e ENCODING encoding ENCODING Read input files using latin or utf8 encoding The default is still latin1 unlit Read literate input files relative positions Just uses the relative library name in positions of warning or errors U FILE xupdate FILE update a development graph according to special XML update informa tion still experimental m FILE modelSparQ FILE model check a qualitative calculus given in SparQ lisp notation 45 aga
27. he top list on the left shows all goal names prefixed with their proof status in square 17 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 mM w uDraw Graph 3 1 1 Development Graph For ToProve Eile Edit Yiew Navigation Abstraction Layout Options Help orrore gt Show node info Show theory Translate theory Taxonomy graphs Show proof status Prove Prove VYSE Structured Disprove Add sentence Check consistency Check conservativity t ke be E ele e Figure 4 Prove local proof obligation Prove ToProve_ToProve v o amp Goals Selected goal s correct Proof details Display Prove incorrect Sublogic of currently selected theory A w CommonLogic FOL Goals All None Invert Select open goals Pick theorem prover SPASS VSE Vampire darwin Selected comorphism path pame gt id_CommonLogic FOL commonLo v Fine grained composition of theory Axioms to include axiom None Invert All Deselect former theorems Show theory Figure 5 Hers Goal and Prover Interface Show selected theory Theorems to include if proven All None invert Close Help Vampire ToProve_ToProve ay w ey Options Timeout Ee Extra Options
28. iguration E a n A Coat cat Timeout 10 v E Show node info ee Show theory v Include Theorems amp Translate theory ii Check ae Taxonomy graphs z k Q Show proof status Sublogic of selected theories Prove CommonLogic FOL en Prove VYSE Structured l Disprove Pick Model Finder Add sentence Isabelle reFute Tae e Check consistency ansia A Check conservativity L darwin non Fd The STOP All None Invert Select comorphism path View results Close Figure 7 Selection of consistency checker Figure 8 Hers Consistency Checker Interface For some selection of nodes of a common logic a model finder should be selectable from the Pick Model finder list Currently only for darwin some Cas models can be re constructed When pressing Check possibly after Select comorphism path all selected nodes will be checked spending at most the number of seconds given under Timeout on each node Pressing Stop allows to terminate this process if too many nodes have been chosen Either by View results or automatically the Results of consistency check Fig 9 will pop up and allow you to inspect the models for nodes if they could be constructed 9 2 Automated Theorem Proving Systems Logic SoftFOL All ATPs integrated into Hets share the same GUI with only a slight modification for the MathServe Broker the input field for extra options is inactive Fig 10 shows the instantiation fo
29. inst a Cas specification References 1 Hets library 2 The OWL API 3 OWL 2 web ontology language Document overview W3C recommendation World Wide Web Consortium W3C October 2009 4 D Aspinal S Berghofer P Callaghan P Courtieu C Rafalli and M Wenzel Emacs Proof General Available athttp proofgeneral inf ed ac uk 5 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 6 Peter Baumgartner Alexander Fuchs and Cesare Tinelli Implementing the Model Evolution Calcu lus In Stephan Schulz Geoff Sutcliffe and Tanel Tammet editors Special Issue of the International Journal of Artificial Intelligence Tools IJAIT volume 15 of International Journal of Artificial Intelli gence Tools 2005 Preprint 7 Dave Beckett RDF XML syntax specification revised W3C recommendation World Wide Web Consortium W3C February 2004 8 David Beckett and Tim Berners Lee Turtle terse RDF triple language W3C team submission World Wide Web Consortium W3C January 2008 9 Christoph Benzmiiller Florian Rabe and Geoff Sutcliffe THFO the core of the TPTP language for higher order logic In Alessandro Armando Peter Baumgartner and Gilles Dowek editors Automated Reasoning 4th International Joint Conference IJCAR 2008 Sydney Australia Aug
30. ively interprets the module Atomless BooleanLattice These two modules specify axioms about booleans thus they have the same signa ture In the graph of imports they have several common imported modules e g BoundedDistributive Lattice but no common importing module as can be seen from Fig For use with Herts we have made a dump of the COLORE contents available in CommonLogic colore in the Hers library 1 The HerCas variant of expressing the relative interpretation can be found in CommonLogic Examples COLORE RelativelInterpretation Here it is not necessary to rename symbols as both modules have the same signature For easier understanding the HerCas implementation includes literal copies of the RegionBoolean ContactAlgebra and AtomlessBooleanLattice modules actually they could as well have been included from their respective files using from get library COLORE RelativeInterpretation logic CommonLogic from CommonLogic colore lat BooleanLattice get BooleanLattice from CommonLogic colore ca BooleanContactAlgebra get BooleanContactAlgebra spec AtomlessBooleanLattice BooleanLattice then forall x 13 exists y and not y end spec RegionBooleanContactAlgebra BooleanContactAlgebra then forall x 1 and not x 0 not x 1 exists y and complement x y C x y end view v AtomlessBooleanLattice to RegionBooleanContactAlgebra 8 2 3 Relative Interpretation Standalone E
31. l as a logic independent parsing and static analysis tool for structured and architectural specifications Actually we are using a revised semantics for modules as proposed recently in 33 and libraries The latter of course needs to call the logic specific tools whenever a basic specification is encountered Herts is based on the theory of institutions 16 which formalise the notion of a logic The theory behind Herts is laid out in 25 A short overview of Hers is given in 27 28 HeEts supports a number of input languages directly such as Common Logic and OWL2 and HerCast They will be described in the next sections 2 1 Common Logic and the Common Logic Interchange Format CLIF CLIF is specified in Annex A of the Common Logic standard 12 Hers can directly read in files in CLIF syntax and also recursively reads in any imported files cf Sect 8 1 for the syntax Common Logic itself does not support the specification of logical consequences nor relative theory interpretations nor other features that speak about structuring and comparing logical theories Michael Grtininger has suggested certain special annotations comments for this purpose which are supported by Hets see Sect Alternatively CLIF syntax can be used for specifications within HetCast files or CLIF files can be referred to within HetCast files HETCasi is a structuring language supporting relative theory interpretations and other things see Sect 2 3 below
32. n Computer Science pages 519 522 Springer Verlag Heidelberg 2007 Till Mossakowski Christian Maeder and Klaus L ttich The Heterogeneous Tool Set In Bernhard Beckert editor VERIFY 2007 volume 259 of CEUR Workshop Proceedings 2007 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 Boris Motik Bernardo Cuenca Grau Ian Horrocks Zhe Wu Achille Fokoue and Carsten Lutz OWL 2 web ontology language Profiles W3C recommendation World Wide Web Consortium W30 October 2009 Boris Motik Bijan Parsia and Peter F Patel Schneider OWL 2 web ontology language XML serial ization W3C recommendation World Wide Web Consortium W3C 10 2009 27 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 Boris Motik Peter F Patel Schneider and Bernardo Cuenca Grau OWL 2 web ontology language Direct semantics W3C recommendation World Wide Web Consortium W3C October 2009 Fabian Neuhaus and Pat Hayes Common logic and the Horatio problem accepted by Applied Ontology 2011 T Nipkow L C Paulson and M Wenzel Isabelle HOL A Proof Assistant for Higher Order Logic Springer Verlag 2002 Peter F Patel Schneider and Boris Motik OWL 2 web ontology language Mapping to RDF graphs W3C recommendation World Wide Web Consortium W3C
33. ndecidable 38 OWL DL all of OWL under the direct semantics 32 and the so called OWL Profiles i e proper sublanguages OWL EL OWL QL and OWL RL 30 Hets supports all except OWL Full The structuring of the OWL imports is displayed as a Development Graph Propositional is classical propositional logic with the zChaff SAT solver connected to it SoftFOL offers several automated theorem proving ATP systems for first order logic with equality 1 Sess ZB sec EEP 7www spass prover ora 2 Darwin B seelhttp combinat in cS uiowa edu Darwin 3 Vampire 87 see http www vprover org 4 Eprover 40 see ht tp www eprover org 5 E KRHyper 36 see and 6 MathServe Broke 47 These together comprise some of the most advanced theorem provers for first order logic SoftFOL is essentially the first order inter change language TPTP I see http www tptp ozg CASL extends many sorted first order logic with partial functions and subsorting It also provides induc tion sentences expressing the free generation of datatypes For more details on Cast see 29 11 For Common Logic Casi can be seen as kind of transitional hub linking Common Logic to other logics most importantly SoftFOL ISABELLE is the logic of the interactive theorem prover Isabelle for higher order logic THF is an interchange language for higher order logic 9 similar to what TPTP is for first order logic Hets con
34. nects THF to the automated higher order prover Leo II HasCASL is a higher order extension of Cast allowing polymorphic datatypes and functions It is closely related to the programming language Haskell and allows program constructs being embedded in the specification For Common Logic HasCas is mainly interesting as a transitional hub for paths to the provers Isabelle and Leo II RelScheme is a logic for relational databases 39 Various logics are supported with proof tools Proof support for the other logics can be obtained by using logic translations to a prover supported logic For Common Logic the paths to SoftFOL are particularly interesting because this offers an interface to standard first order provers Moreover the paths to THF and Isabelle offer interfaces to higher order provers which is essential if you want to prove inductive theorems about sequences An introduction to Casi can be found in the Casi User Manual the detailed language reference is given in the Cast Reference Manual 29 These documents explain both the Cast logic and language of basic specifications as well as the logic independent constructs for structured and architectural spec ifications The corresponding document explaining the HerCas language constructs for heterogeneous structured specifications is the HerCas language summary 24 a formal semantics as well as a user manual with more examples are in preparation Some of HeEtTCast s heterogeneous constr
35. oftFOLInduction Same as CASL2SoftFOL but with instances of induction axioms for all proof goals CASL2SoftFOLInduction2 Similar to CASL2SoftFOLInduction but replaces goals with induc tion premises CASL2Propositional Translation of propositional FOL Those comorphisms can be chained e g for theorem proving you can translate Common Logic to SoftFOL with CommonLogic2CASLCompact CASL2SoftFOLInduction since there is no prover for Common Logic or CAsL For further information on logic translations supported by Herts see the Hers user guide 44 5 Getting started The latest Herts version can be obtained from the Hers tools home page http www dfki de sks hets Since Herts is being improved constantly it is recommended always to use the latest version Hets is currently available on Intel architectures only for Linux and Mac OS X There are several possibilities to install Hers 1 The best support is currently given via Ubuntu packages For Ubuntu Lucid Lynx enter the following into a terminal sudo apt add repository ppa hets hets sudo apt add repository deb http archive canonical com ubuntu lucid partner sudo apt get update sudo apt get install hets For later Ubuntu versions replace lucid by maverick natty or oneiric This will also install quite a couple of tools for proving requiring about 800 MB of disk space For a minimal installation use apt get install hets core instead of hets 2 For Mac OS X 10 6
36. ogy cover the core of these concepts they provide at least classes or generic superclasses corresponding to the concepts highlighted in bold However that does not cover the scenario completely In particular there are relevant concepts here space and time underlined which are not covered at the required level of complexity OpenAAL says that appointments have a date and that rooms can be connected to each other but not what ex actly that means Foundational ontologies and spatial calculi often formalized in first order logic cover space and time at the level of complexity required by a central controller of an apartment and by an autonomously navigating wheelchair More concretely Common Logic is useful in this scenario for expressing knowledge on the arrange ment of rooms e g as follows in a first order formalization of an RCC style spatial calculus Va 1 a2 equal a a2 V overlapping a 1 a2 Y bordering a a2 V disconnected a a2 Y proper _part_of a1 a2 Y proper_part_of a2 a1 Two areas in a house e g a working area in a room are either the same or intersecting or bordering or separated or one is a proper part of the other The following listing shows a relevant excerpt of the heterogeneous specification which can be found under Ontology Examples AAL het in the Hers library 1 The key features include e Heterogeneous specification allows for reusing the OpenAAL OWL ontology but at the same time form
37. omdoc HOT CIT clr xml tree gen_trm baf O DIR output dir DIR Specify DIR as destination directory for output files o OTYPES output types OTYPES OTYPES is a comma separated list of output types 23 Orr env omn LIT omdoc xml exp hs thy comptable xml sig th delta pp het tex xml html graph exp dot dot dig c tptpl c The env and prf formats are for subsequent reading avoiding the need to re analyse downloaded libraries prf files can also be stored or loaded via the GUI s File menu The omn option will produce OWL files in Manchester Syntax for each specification of a struc tured OWL library The clif option will produce Common Logic files in CLIF dialect for each specification of a Com mon Logic library The omdoc format is an XML based markup format and data model for Open Mathematical Documents It serves as semantics oriented representation format and ontology language for math ematical knowledge Although this is still in experimental state Common Logic theories can be exported to and imported from OMDoc The xml option will produce an XML version of the development graph for our change management broker The exp format is the new experimental omdoc format The hs format is used for Haskell modules Executable Casi or HasCasi specifications can be trans lated to Haskell When the thy format is selected Hers will try to translate each speci
38. ove mentioned software and set several environment variables as explained on the installation page 5 You may compile Herts from the sources they are licensed under GPL please follow the link Hets source code and information for developers on the Hers web page download the sources as tarball or from svn and follow the instructions in the INSTALL file but be prepared to take some time Depending on your application further tools are supported and may be installed in addition zhat SAT sover http Jwaw princeton edu chaff achaff hen minist SAT solver m minisat se7 SSCS Pellet OWL reasoner nttp clarkparsia con peliet S E KRHyper theorem prover lnttp userpages uni koblenz de bpelzer ekahyper Reduce computer algebra system http waw reduce algebra com SS Maude rewrite system http maude cs wiuc edu SSS VIwelf O eoe plparty org SOS 6 Analysis of Specifications Consider the following Common Logic text written in CLIF P x and P x Q y or Cat x Mat y not On x y I P x 10 2 exists z and Pet x Happy z Attr x z Hets can be used for parsing and checking static well formedness of specifications Let us assume that the example is in a file named Cat AllInOne clif Then you can check the well formedness of the specification by typing into some shell hets Cat AllInOne clif Hets checks both the correctness of this sp
39. r Spass where in the top right part of the window the batch mode can be controlled The left side shows the list of goals with status indicators If goals are timed out indicated by t it may help to activate the check box Include preceding proven theorems in next proof attempt and pressing Prove all again On the bottom right the result of the last proof attempt is displayed The Status indicates Open Proved Disproved Open Time is up or Proved Theory inconsistent The list of Used Axioms is filled by Spass The button Show Details shows the whole output of the ATP system The Save buttons allow you to save the input and configuration of each proof for documentation By Close the results for all goals are transferred back to the Proof Management GUI The MathServe system developed by Jiirgen Zimmer provides a unified interface to a range of different ATP systems the most important systems are listed in Tab 1 along with their capabilities 20 A Results of consistency check v B x Nodes Result consistent but could not reconstruct a model extractModel not implemented For comorphism composition with id_CommonLogic FOL CommonLogic2CASLCompact CASL2SubCFOL SatisFiable Darwin 1 4 4 Finite Domain setting initial domain size to 1 Finite Domain using non ground splitting in preprocessing Parsing tmp cat_cat9010 tptp Calling eprover For clausific
40. rrow in the development graph Just as with imports 8 1 Hers supports different types of references to resources here as e g URIs Inclusion is not a relation between theories However inclusion can useful It is used to show other theories in the development graph without any connection to the current theory For loading such theories HerCas employs the same syntax as for loading theories that are con nected to other theories i e on loading theories Hers does not care about their relations 11 from library get spec specy Except for importation and inclusion you can specify an optional symbol map name map in a relation Names from the target file are mapped to names from the current file including the translation file if the relation uses one Note that is is possible to use cyclic relations in Hers Only the cyclic importation is not supported 8 2 Examples This section introduces several typical examples of using Common Logic ontologies with Herts 8 2 1 Renaming Symbols with Symbol Maps This example has two almost identical Common Logic texts upper clif and lower clif these can be found in the CommonLogic Examples directory in the Hers library 1 The only difference in the actual axioms is that upper clif uses uppercase predicates while lower clif uses lowercase predicates upper clif cl text upper forall x y iff A B x y x lt lower clif cl text lower forall x y iff a b
41. ry g gui shows the development graph in a GUI window u uncolored no colours in shown graphs The following additional options also apply typical rules from the development graph calculus to the final graph and save applying these rules via the GUI A apply automatic rule apply the automatic strategy to the development graph This is what you usually want in order to get goals within nodes for proving N normal form compute all normal forms for nodes with incoming hiding links This may take long and may not be implemented for all logics For a summary of the types of nodes and links occurring in development graphs see the Herts user guide Most of the pull down menus of the development graph window are uDraw Graph specific layout menus their function can be looked up in the uDraw Graph documentation The Edit menu is the only exception With choosing Edit Proofs Auto DG prover you can can prove red theorem links which may be generated by relative interpretations of theories Actually this will generate new proof obligations at some node which then can be discharged there Moreover the nodes and links of the graph have attached pop up menus which appear when clicking and holding the right mouse button The node menus Prove and Check consistency are the most important ones With Add sentence you can add axioms and proof goals on the fly For a detailed explanation of the menus see the H
42. sproven Note that they are separate texts inside the specification ToProve The annotations are optional For proving they are the names shown in the Axioms to include section of the prover interface Fig 5 The same specification can be written down in CLIF cl text axiom P x and P x Q y cl text correct Q y Simplied cl text incorrect P y implied 10HelloWorldExamples ToProve het in the HETS library 1 19 In CLIF there is no notion of proof obligation Hence the implied keyword of Hers must be used and thus the specification is not pure CLIF Because the texts have names these are also used in the prover interface Otherwise Herts invents names 9 1 Consistency Checker Since proofs are void if specifications are inconsistent the consistency should be checked if possible for the given logic by the Consistency checker shown in Fig 8 This GUI is invoked from the Edit menu as it operates on all nodes The list on the left shows all node names prefixed with a consistency status in square brackets that is initially empty A consistent node is indicated by a a indicates an inconsistent node a t denotes a timeout of the last checking attempt Mm amp uDraw Graph 3 1 1 Development Graph For cat y o amp Eile Edit Yiew Navigation Abstraction Layout Options sai j X Consistency Checker Nodes or goals Checker Conf
43. the specification does not contain any sequence markers it is possible to use the comorphism CommonLogic2CASLCompact which results in a simpler Casi specification We recommend using this comorphism whenever possible e 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 in the bottom lists the axioms and proven theorems that will comprise the theory of the next proof attempt Based on this selection the sublogic may vary and so do the available provers and the comorphism paths leading to provers Former theorems that are imported 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 e If you press the bottom right 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 e All other buttons control selecting list entries In order to prove or disprove a theorem it needs to be declared as proof obligation This is done by the keyword implied at the end of a text logic CommonLogic spec ToProve P x and P x Q y Q y sSimplied correct P y Simplied incorrect end In this specificatior the theorems annotated named by correct and incorrect are the ones that can be proven or di
44. tps someDomain com path to someFile clif The importation is indicated by a global definition link black arrow in the development graph Relative interpretation is formally defined in 19 Informally one module relatively interprets those modules whose theorems are preserved within the current module through a mapping There exists a mapping between modules such that all theorems of the other module hold in the current module after the mapping is applied 18 HrrTs represents relative interpretation by a theorem link red arrow in the development graph The HerTCas syntax for relative interpretations is view v someCLText to someTargetCLText end or view v someCLText with lt symbol map see below gt to someTargetCLText end where a symbol map allows for renaming symbols e g namelOld gt namelNew name2Old gt name2New We provide a concrete examples in Sect 8 2 below Just as with imports see above Hers supports different types of references to resources here such as URIs Non conservative extension is informally defined as follows One module non conservatively extends other modules if its axioms entail new facts for the shared lexicon of the other module s That is the shared lexicon between the current module and a non conservatively extended module are not logically equivalent with respect to their modules 18 HETs represents non conservative extension by a theorem link red a
45. ucts will be il lustrated in Sect 7 below For further information on logics supported by Hers see the Herts user guide 44 3which chooses an appropriate ATP upon a classification of the FOL problem 4 Logic translations supported by Hets Logic translations formalised as institution comorphisms 15 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 In more detail the following list of logic translations involving Common Logic is currently supported by Herts CommonLogic2CASL Coding Common Logic to Cas_ Module elimination is applied be fore translating to Cast CommonLogic2CASLCompact Coding compact Common Logic to Cast Compact Common Logic is a sublogic of Common Logic where no sequence markers oc cur Module elimination is applied before translating to Cas We recommend using this comorphism whenever possible because it results in simpler specifications CommonLogicModuleElimination Eliminating modules from a Common Logic theory resulting in an equivalent specification without modules OWL22CommonLogic Inclusion of OWL2 description logic Prop2CommonLogic Inclusion of propositional logic SoftFOL2CommonLogic Inclusion of first order logic CASL2SoftFOL Coding of CASL SuleCFOL E to SoftFOL 23 mapping types to soft types CASL2S
46. ust 12 15 2008 Proceedings volume 5195 of Lecture Notes in Computer Science pages 491 506 Springer 2008 10 T Berners Lee J Hendler and O Lassila The Semantic Web Scientific American May 2001 11 M Bidoit and P D Mosses CASL User Manual volume 2900 of LNCS Springer 2004 Free online version available at ht tp www cofi info 12 Information technology Common Logic CL a framework for a family of logic based languages Technical Report 24707 2007 ISO IEC 2007 26 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 Current defect report for iso iec 24707 2007 Technical report ISO IEC 2008 Free Software Foundation Emacs Available at http www gnu org software emacs J Goguen and G Ro u Institution morphisms Formal aspects of computing 13 274 307 2002 J A Goguen and R M Burstall Institutions Abstract model theory for specification and program ming Journal of the Association for Computing Machinery 39 95 146 1992 Predecessor in LNCS 164 221 256 1984 M Gruninger COLORE Common Logic Repository Available at http st1 mie utoronto M Gruninger et al COLORE metadata definitions Available at http stl mie utoronto ca colore metadata html Michael Gruninger Torsten Hahmann Ali Hashemi and Darren Ong Ontology verification with repositories In Antony Galton and
47. xample This example defines a partial order twice once as an extension of a strict partial order and once directly Then we connect both definitions by a view that expresses the relative interpretation The source is available as CommonLogic Examples Partial_Orders het directory in the HETS library 1 logic CommonLogic spec Strict_Partial_Order 6 strict forall x not lt x x asymmetric forall x y if lt x y not lt y x 6 transitive forall x y z if and lt x y oe yY 2 1 X Z end spec Partial_Order_ From strict_Partial_ Order Strict_Partial_Order then 2 define less or equal in terms of less than forall x y iff le x y or lt x y x y end spec Partial_Order 14 3 reflexive forall x le x x antisymmetric forall x y if and le x y le y X x yY 3 transitive forall x y z if and le x y le y zZ le x Z end view v Partial Order to Partial Order From Strict Partial Order 8 2 4 Ontology based Ambient Assisted Living Services and Devices Consider the following ambient assisted living AAL scenario Clara instructs her wheelchair to get her to the kitchen next door to the living room For dinner she would like to take a pizza from the freezer and bake it in the oven Her diet is vegetarian Afterwards she needs to rest in bed Existing ontologies for ambient assisted living e g the OpenAAL OWL ontol
Download Pdf Manuals
Related Search