GenZ (empty) → 0.1.0.0
raw patch · 33 files changed
+4254/−0 lines, 33 filesdep +GenZdep +QuickCheckdep +array
Dependencies added: GenZ, QuickCheck, array, base, bytestring, cassava, containers, criterion, directory, file-embed, filepath, graphviz, hspec, js-jquery, multiset, optparse-applicative, process, random, scientific, scotty, split, tagged, template-haskell, temporary, text, vector, warp, weigh
Files
- GenZ.cabal +289/−0
- LICENSE +674/−0
- README.md +250/−0
- bench/memory.hs +46/−0
- bench/runtime.hs +126/−0
- exec/form-size.hs +17/−0
- exec/genz-web.hs +118/−0
- exec/genz.hs +194/−0
- exec/index.html +248/−0
- exec/tptp-size.hs +15/−0
- lib/Basics.hs +75/−0
- lib/FormM.hs +245/−0
- lib/FormM/Parse.y +85/−0
- lib/FormP.hs +220/−0
- lib/FormP/Parse.y +73/−0
- lib/FormP/ParseTPTP.hs +143/−0
- lib/General.hs +404/−0
- lib/General/Lex.x +71/−0
- lib/General/Token.hs +23/−0
- lib/Logic/Modal/D.hs +26/−0
- lib/Logic/Modal/D4.hs +21/−0
- lib/Logic/Modal/D45.hs +48/−0
- lib/Logic/Modal/GL.hs +30/−0
- lib/Logic/Modal/K.hs +45/−0
- lib/Logic/Modal/K4.hs +29/−0
- lib/Logic/Modal/K45.hs +66/−0
- lib/Logic/Modal/S4.hs +21/−0
- lib/Logic/Modal/T.hs +40/−0
- lib/Logic/Propositional/CPL.hs +35/−0
- lib/Logic/Propositional/IPL.hs +82/−0
- package.yaml +115/−0
- stack.yaml +1/−0
- test/Test.hs +379/−0
+ GenZ.cabal view
@@ -0,0 +1,289 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.39.1.+--+-- see: https://github.com/sol/hpack++name: GenZ+version: 0.1.0.0+synopsis: Generic Sequent Calculus Prover using the Zipper+description: See README.md for example usage and documentation.+category: Logic+homepage: https://github.com/XiaoshuangYang999/GenZ#readme+bug-reports: https://github.com/XiaoshuangYang999/GenZ/issues+maintainer: Xiaoshuang Yang <thuyxs17@gmail.com>+license: GPL-3+license-file: LICENSE+build-type: Simple+extra-source-files:+ README.md+ LICENSE+ stack.yaml+ package.yaml+ lib/FormM/Parse.y+ lib/FormP/Parse.y+ lib/General/Lex.x+ exec/index.html++source-repository head+ type: git+ location: https://github.com/XiaoshuangYang999/GenZ++library+ exposed-modules:+ Basics+ FormM+ FormM.Parse+ FormP+ FormP.Parse+ FormP.ParseTPTP+ General+ General.Lex+ General.Token+ Logic.Modal.D+ Logic.Modal.D4+ Logic.Modal.D45+ Logic.Modal.GL+ Logic.Modal.K+ Logic.Modal.K4+ Logic.Modal.K45+ Logic.Modal.S4+ Logic.Modal.T+ Logic.Propositional.CPL+ Logic.Propositional.IPL+ other-modules:+ Paths_GenZ+ hs-source-dirs:+ lib+ ghc-options: -Wall+ build-tools:+ alex+ , happy+ build-depends:+ QuickCheck >=2.4.3 && <2.19+ , array >=0.5.4 && <0.6+ , base >=4.8 && <5+ , bytestring >=0.11.5 && <0.12+ , containers >=0.6.7 && <0.7+ , directory >=1.3.7 && <1.4+ , filepath >=1.4.2 && <1.5+ , graphviz >=2999.20.2 && <2999.21+ , hspec >=2.10.10 && <2.12+ , multiset >=0.3.4 && <0.4+ , process >=1.6.18 && <1.7+ , random >=1.2.1 && <1.4+ , tagged >=0.8.7 && <0.9+ , temporary ==1.3.*+ default-language: Haskell2010++executable form-size+ main-is: form-size.hs+ other-modules:+ Paths_GenZ+ hs-source-dirs:+ exec+ ghc-options: -Wall -Wall -threaded+ build-tools:+ alex+ , happy+ build-depends:+ GenZ+ , QuickCheck >=2.4.3 && <2.19+ , array >=0.5.4 && <0.6+ , base >=4.8 && <5+ , bytestring >=0.11.5 && <0.12+ , containers >=0.6.7 && <0.7+ , directory >=1.3.7 && <1.4+ , filepath >=1.4.2 && <1.5+ , graphviz >=2999.20.2 && <2999.21+ , hspec >=2.10.10 && <2.12+ , multiset >=0.3.4 && <0.4+ , process >=1.6.18 && <1.7+ , random >=1.2.1 && <1.4+ , tagged >=0.8.7 && <0.9+ , temporary ==1.3.*+ default-language: Haskell2010++executable genz+ main-is: genz.hs+ other-modules:+ Paths_GenZ+ hs-source-dirs:+ exec+ ghc-options: -Wall -Wall -threaded+ build-tools:+ alex+ , happy+ build-depends:+ GenZ+ , QuickCheck >=2.4.3 && <2.19+ , array >=0.5.4 && <0.6+ , base >=4.8 && <5+ , bytestring >=0.11.5 && <0.12+ , containers >=0.6.7 && <0.7+ , directory >=1.3.7 && <1.4+ , filepath >=1.4.2 && <1.5+ , graphviz >=2999.20.2 && <2999.21+ , hspec >=2.10.10 && <2.12+ , multiset >=0.3.4 && <0.4+ , optparse-applicative >=0.17.1 && <0.18+ , process >=1.6.18 && <1.7+ , random >=1.2.1 && <1.4+ , tagged >=0.8.7 && <0.9+ , temporary ==1.3.*+ default-language: Haskell2010++executable genz-web+ main-is: genz-web.hs+ other-modules:+ Paths_GenZ+ hs-source-dirs:+ exec+ ghc-options: -Wall -Wall -threaded+ build-tools:+ alex+ , happy+ build-depends:+ GenZ+ , QuickCheck >=2.4.3 && <2.19+ , array >=0.5.4 && <0.6+ , base >=4.8 && <5+ , bytestring >=0.11.5 && <0.12+ , containers >=0.6.7 && <0.7+ , directory >=1.3.7 && <1.4+ , file-embed >=0.0.15 && <0.1+ , filepath >=1.4.2 && <1.5+ , graphviz >=2999.20.2 && <2999.21+ , hspec >=2.10.10 && <2.12+ , js-jquery >=3.3.1 && <4+ , multiset >=0.3.4 && <0.4+ , process >=1.6.18 && <1.7+ , random >=1.2.1 && <1.4+ , scotty ==0.12.*+ , tagged >=0.8.7 && <0.9+ , template-haskell >=2.19.0 && <2.21+ , temporary ==1.3.*+ , text >=2.0.2 && <2.1+ , warp >=3.3.25 && <3.5+ default-language: Haskell2010++executable tptp-size+ main-is: tptp-size.hs+ other-modules:+ Paths_GenZ+ hs-source-dirs:+ exec+ ghc-options: -Wall -Wall -threaded+ build-tools:+ alex+ , happy+ build-depends:+ GenZ+ , QuickCheck >=2.4.3 && <2.19+ , array >=0.5.4 && <0.6+ , base >=4.8 && <5+ , bytestring >=0.11.5 && <0.12+ , containers >=0.6.7 && <0.7+ , directory >=1.3.7 && <1.4+ , filepath >=1.4.2 && <1.5+ , graphviz >=2999.20.2 && <2999.21+ , hspec >=2.10.10 && <2.12+ , multiset >=0.3.4 && <0.4+ , process >=1.6.18 && <1.7+ , random >=1.2.1 && <1.4+ , tagged >=0.8.7 && <0.9+ , temporary ==1.3.*+ default-language: Haskell2010++test-suite Test+ type: exitcode-stdio-1.0+ main-is: Test.hs+ other-modules:+ Paths_GenZ+ hs-source-dirs:+ test+ ghc-options: -Wall -Wall -threaded -rtsopts -with-rtsopts=-N+ build-tools:+ alex+ , happy+ build-depends:+ GenZ+ , QuickCheck >=2.14.3 && <2.15+ , array >=0.5.4 && <0.6+ , base >=4.8 && <5+ , bytestring >=0.11.5 && <0.12+ , containers >=0.6.7 && <0.7+ , directory >=1.3.7 && <1.4+ , filepath >=1.4.2 && <1.5+ , graphviz >=2999.20.2 && <2999.21+ , hspec+ , multiset >=0.3.4 && <0.4+ , process >=1.6.18 && <1.7+ , random >=1.2.1 && <1.4+ , tagged >=0.8.7 && <0.9+ , temporary ==1.3.*+ default-language: Haskell2010++benchmark memory+ type: exitcode-stdio-1.0+ main-is: memory.hs+ other-modules:+ Paths_GenZ+ hs-source-dirs:+ bench+ ghc-options: -Wall -rtsopts+ build-tools:+ alex+ , happy+ build-depends:+ GenZ+ , QuickCheck >=2.4.3 && <2.19+ , array >=0.5.4 && <0.6+ , base >=4.8 && <5+ , bytestring >=0.11.5 && <0.12+ , containers >=0.6.7 && <0.7+ , directory >=1.3.7 && <1.4+ , filepath >=1.4.2 && <1.5+ , graphviz >=2999.20.2 && <2999.21+ , hspec >=2.10.10 && <2.12+ , multiset >=0.3.4 && <0.4+ , process >=1.6.18 && <1.7+ , random >=1.2.1 && <1.4+ , tagged >=0.8.7 && <0.9+ , temporary ==1.3.*+ , weigh+ default-language: Haskell2010++benchmark runtime+ type: exitcode-stdio-1.0+ main-is: runtime.hs+ other-modules:+ Paths_GenZ+ hs-source-dirs:+ bench+ ghc-options: -Wall+ build-tools:+ alex+ , happy+ build-depends:+ GenZ+ , QuickCheck >=2.4.3 && <2.19+ , array >=0.5.4 && <0.6+ , base >=4.8 && <5+ , bytestring+ , cassava+ , containers >=0.6.7 && <0.7+ , criterion+ , directory+ , filepath >=1.4.2 && <1.5+ , graphviz >=2999.20.2 && <2999.21+ , hspec >=2.10.10 && <2.12+ , multiset >=0.3.4 && <0.4+ , process >=1.6.18 && <1.7+ , random >=1.2.1 && <1.4+ , scientific+ , split+ , tagged >=0.8.7 && <0.9+ , temporary ==1.3.*+ , vector+ default-language: Haskell2010
+ LICENSE view
@@ -0,0 +1,674 @@+ GNU GENERAL PUBLIC LICENSE+ Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++ Preamble++ The GNU General Public License is a free, copyleft license for+software and other kinds of works.++ The licenses for most software and other practical works are designed+to take away your freedom to share and change the works. By contrast,+the GNU General Public License is intended to guarantee your freedom to+share and change all versions of a program--to make sure it remains free+software for all its users. We, the Free Software Foundation, use the+GNU General Public License for most of our software; it applies also to+any other work released this way by its authors. You can apply it to+your programs, too.++ When we speak of free software, we are referring to freedom, not+price. Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+them if you wish), that you receive source code or can get it if you+want it, that you can change the software or use pieces of it in new+free programs, and that you know you can do these things.++ To protect your rights, we need to prevent others from denying you+these rights or asking you to surrender the rights. Therefore, you have+certain responsibilities if you distribute copies of the software, or if+you modify it: responsibilities to respect the freedom of others.++ For example, if you distribute copies of such a program, whether+gratis or for a fee, you must pass on to the recipients the same+freedoms that you received. You must make sure that they, too, receive+or can get the source code. And you must show them these terms so they+know their rights.++ Developers that use the GNU GPL protect your rights with two steps:+(1) assert copyright on the software, and (2) offer you this License+giving you legal permission to copy, distribute and/or modify it.++ For the developers' and authors' protection, the GPL clearly explains+that there is no warranty for this free software. For both users' and+authors' sake, the GPL requires that modified versions be marked as+changed, so that their problems will not be attributed erroneously to+authors of previous versions.++ Some devices are designed to deny users access to install or run+modified versions of the software inside them, although the manufacturer+can do so. This is fundamentally incompatible with the aim of+protecting users' freedom to change the software. The systematic+pattern of such abuse occurs in the area of products for individuals to+use, which is precisely where it is most unacceptable. Therefore, we+have designed this version of the GPL to prohibit the practice for those+products. If such problems arise substantially in other domains, we+stand ready to extend this provision to those domains in future versions+of the GPL, as needed to protect the freedom of users.++ Finally, every program is threatened constantly by software patents.+States should not allow patents to restrict development and use of+software on general-purpose computers, but in those that do, we wish to+avoid the special danger that patents applied to a free program could+make it effectively proprietary. To prevent this, the GPL assures that+patents cannot be used to render the program non-free.++ The precise terms and conditions for copying, distribution and+modification follow.++ TERMS AND CONDITIONS++ 0. Definitions.++ "This License" refers to version 3 of the GNU General Public License.++ "Copyright" also means copyright-like laws that apply to other kinds of+works, such as semiconductor masks.++ "The Program" refers to any copyrightable work licensed under this+License. Each licensee is addressed as "you". "Licensees" and+"recipients" may be individuals or organizations.++ To "modify" a work means to copy from or adapt all or part of the work+in a fashion requiring copyright permission, other than the making of an+exact copy. The resulting work is called a "modified version" of the+earlier work or a work "based on" the earlier work.++ A "covered work" means either the unmodified Program or a work based+on the Program.++ To "propagate" a work means to do anything with it that, without+permission, would make you directly or secondarily liable for+infringement under applicable copyright law, except executing it on a+computer or modifying a private copy. Propagation includes copying,+distribution (with or without modification), making available to the+public, and in some countries other activities as well.++ To "convey" a work means any kind of propagation that enables other+parties to make or receive copies. Mere interaction with a user through+a computer network, with no transfer of a copy, is not conveying.++ An interactive user interface displays "Appropriate Legal Notices"+to the extent that it includes a convenient and prominently visible+feature that (1) displays an appropriate copyright notice, and (2)+tells the user that there is no warranty for the work (except to the+extent that warranties are provided), that licensees may convey the+work under this License, and how to view a copy of this License. If+the interface presents a list of user commands or options, such as a+menu, a prominent item in the list meets this criterion.++ 1. Source Code.++ The "source code" for a work means the preferred form of the work+for making modifications to it. "Object code" means any non-source+form of a work.++ A "Standard Interface" means an interface that either is an official+standard defined by a recognized standards body, or, in the case of+interfaces specified for a particular programming language, one that+is widely used among developers working in that language.++ The "System Libraries" of an executable work include anything, other+than the work as a whole, that (a) is included in the normal form of+packaging a Major Component, but which is not part of that Major+Component, and (b) serves only to enable use of the work with that+Major Component, or to implement a Standard Interface for which an+implementation is available to the public in source code form. A+"Major Component", in this context, means a major essential component+(kernel, window system, and so on) of the specific operating system+(if any) on which the executable work runs, or a compiler used to+produce the work, or an object code interpreter used to run it.++ The "Corresponding Source" for a work in object code form means all+the source code needed to generate, install, and (for an executable+work) run the object code and to modify the work, including scripts to+control those activities. However, it does not include the work's+System Libraries, or general-purpose tools or generally available free+programs which are used unmodified in performing those activities but+which are not part of the work. For example, Corresponding Source+includes interface definition files associated with source files for+the work, and the source code for shared libraries and dynamically+linked subprograms that the work is specifically designed to require,+such as by intimate data communication or control flow between those+subprograms and other parts of the work.++ The Corresponding Source need not include anything that users+can regenerate automatically from other parts of the Corresponding+Source.++ The Corresponding Source for a work in source code form is that+same work.++ 2. Basic Permissions.++ All rights granted under this License are granted for the term of+copyright on the Program, and are irrevocable provided the stated+conditions are met. This License explicitly affirms your unlimited+permission to run the unmodified Program. The output from running a+covered work is covered by this License only if the output, given its+content, constitutes a covered work. This License acknowledges your+rights of fair use or other equivalent, as provided by copyright law.++ You may make, run and propagate covered works that you do not+convey, without conditions so long as your license otherwise remains+in force. You may convey covered works to others for the sole purpose+of having them make modifications exclusively for you, or provide you+with facilities for running those works, provided that you comply with+the terms of this License in conveying all material for which you do+not control copyright. Those thus making or running the covered works+for you must do so exclusively on your behalf, under your direction+and control, on terms that prohibit them from making any copies of+your copyrighted material outside their relationship with you.++ Conveying under any other circumstances is permitted solely under+the conditions stated below. Sublicensing is not allowed; section 10+makes it unnecessary.++ 3. Protecting Users' Legal Rights From Anti-Circumvention Law.++ No covered work shall be deemed part of an effective technological+measure under any applicable law fulfilling obligations under article+11 of the WIPO copyright treaty adopted on 20 December 1996, or+similar laws prohibiting or restricting circumvention of such+measures.++ When you convey a covered work, you waive any legal power to forbid+circumvention of technological measures to the extent such circumvention+is effected by exercising rights under this License with respect to+the covered work, and you disclaim any intention to limit operation or+modification of the work as a means of enforcing, against the work's+users, your or third parties' legal rights to forbid circumvention of+technological measures.++ 4. Conveying Verbatim Copies.++ You may convey verbatim copies of the Program's source code as you+receive it, in any medium, provided that you conspicuously and+appropriately publish on each copy an appropriate copyright notice;+keep intact all notices stating that this License and any+non-permissive terms added in accord with section 7 apply to the code;+keep intact all notices of the absence of any warranty; and give all+recipients a copy of this License along with the Program.++ You may charge any price or no price for each copy that you convey,+and you may offer support or warranty protection for a fee.++ 5. Conveying Modified Source Versions.++ You may convey a work based on the Program, or the modifications to+produce it from the Program, in the form of source code under the+terms of section 4, provided that you also meet all of these conditions:++ a) The work must carry prominent notices stating that you modified+ it, and giving a relevant date.++ b) The work must carry prominent notices stating that it is+ released under this License and any conditions added under section+ 7. This requirement modifies the requirement in section 4 to+ "keep intact all notices".++ c) You must license the entire work, as a whole, under this+ License to anyone who comes into possession of a copy. This+ License will therefore apply, along with any applicable section 7+ additional terms, to the whole of the work, and all its parts,+ regardless of how they are packaged. This License gives no+ permission to license the work in any other way, but it does not+ invalidate such permission if you have separately received it.++ d) If the work has interactive user interfaces, each must display+ Appropriate Legal Notices; however, if the Program has interactive+ interfaces that do not display Appropriate Legal Notices, your+ work need not make them do so.++ A compilation of a covered work with other separate and independent+works, which are not by their nature extensions of the covered work,+and which are not combined with it such as to form a larger program,+in or on a volume of a storage or distribution medium, is called an+"aggregate" if the compilation and its resulting copyright are not+used to limit the access or legal rights of the compilation's users+beyond what the individual works permit. Inclusion of a covered work+in an aggregate does not cause this License to apply to the other+parts of the aggregate.++ 6. Conveying Non-Source Forms.++ You may convey a covered work in object code form under the terms+of sections 4 and 5, provided that you also convey the+machine-readable Corresponding Source under the terms of this License,+in one of these ways:++ a) Convey the object code in, or embodied in, a physical product+ (including a physical distribution medium), accompanied by the+ Corresponding Source fixed on a durable physical medium+ customarily used for software interchange.++ b) Convey the object code in, or embodied in, a physical product+ (including a physical distribution medium), accompanied by a+ written offer, valid for at least three years and valid for as+ long as you offer spare parts or customer support for that product+ model, to give anyone who possesses the object code either (1) a+ copy of the Corresponding Source for all the software in the+ product that is covered by this License, on a durable physical+ medium customarily used for software interchange, for a price no+ more than your reasonable cost of physically performing this+ conveying of source, or (2) access to copy the+ Corresponding Source from a network server at no charge.++ c) Convey individual copies of the object code with a copy of the+ written offer to provide the Corresponding Source. This+ alternative is allowed only occasionally and noncommercially, and+ only if you received the object code with such an offer, in accord+ with subsection 6b.++ d) Convey the object code by offering access from a designated+ place (gratis or for a charge), and offer equivalent access to the+ Corresponding Source in the same way through the same place at no+ further charge. You need not require recipients to copy the+ Corresponding Source along with the object code. If the place to+ copy the object code is a network server, the Corresponding Source+ may be on a different server (operated by you or a third party)+ that supports equivalent copying facilities, provided you maintain+ clear directions next to the object code saying where to find the+ Corresponding Source. Regardless of what server hosts the+ Corresponding Source, you remain obligated to ensure that it is+ available for as long as needed to satisfy these requirements.++ e) Convey the object code using peer-to-peer transmission, provided+ you inform other peers where the object code and Corresponding+ Source of the work are being offered to the general public at no+ charge under subsection 6d.++ A separable portion of the object code, whose source code is excluded+from the Corresponding Source as a System Library, need not be+included in conveying the object code work.++ A "User Product" is either (1) a "consumer product", which means any+tangible personal property which is normally used for personal, family,+or household purposes, or (2) anything designed or sold for incorporation+into a dwelling. In determining whether a product is a consumer product,+doubtful cases shall be resolved in favor of coverage. For a particular+product received by a particular user, "normally used" refers to a+typical or common use of that class of product, regardless of the status+of the particular user or of the way in which the particular user+actually uses, or expects or is expected to use, the product. A product+is a consumer product regardless of whether the product has substantial+commercial, industrial or non-consumer uses, unless such uses represent+the only significant mode of use of the product.++ "Installation Information" for a User Product means any methods,+procedures, authorization keys, or other information required to install+and execute modified versions of a covered work in that User Product from+a modified version of its Corresponding Source. The information must+suffice to ensure that the continued functioning of the modified object+code is in no case prevented or interfered with solely because+modification has been made.++ If you convey an object code work under this section in, or with, or+specifically for use in, a User Product, and the conveying occurs as+part of a transaction in which the right of possession and use of the+User Product is transferred to the recipient in perpetuity or for a+fixed term (regardless of how the transaction is characterized), the+Corresponding Source conveyed under this section must be accompanied+by the Installation Information. But this requirement does not apply+if neither you nor any third party retains the ability to install+modified object code on the User Product (for example, the work has+been installed in ROM).++ The requirement to provide Installation Information does not include a+requirement to continue to provide support service, warranty, or updates+for a work that has been modified or installed by the recipient, or for+the User Product in which it has been modified or installed. Access to a+network may be denied when the modification itself materially and+adversely affects the operation of the network or violates the rules and+protocols for communication across the network.++ Corresponding Source conveyed, and Installation Information provided,+in accord with this section must be in a format that is publicly+documented (and with an implementation available to the public in+source code form), and must require no special password or key for+unpacking, reading or copying.++ 7. Additional Terms.++ "Additional permissions" are terms that supplement the terms of this+License by making exceptions from one or more of its conditions.+Additional permissions that are applicable to the entire Program shall+be treated as though they were included in this License, to the extent+that they are valid under applicable law. If additional permissions+apply only to part of the Program, that part may be used separately+under those permissions, but the entire Program remains governed by+this License without regard to the additional permissions.++ When you convey a copy of a covered work, you may at your option+remove any additional permissions from that copy, or from any part of+it. (Additional permissions may be written to require their own+removal in certain cases when you modify the work.) You may place+additional permissions on material, added by you to a covered work,+for which you have or can give appropriate copyright permission.++ Notwithstanding any other provision of this License, for material you+add to a covered work, you may (if authorized by the copyright holders of+that material) supplement the terms of this License with terms:++ a) Disclaiming warranty or limiting liability differently from the+ terms of sections 15 and 16 of this License; or++ b) Requiring preservation of specified reasonable legal notices or+ author attributions in that material or in the Appropriate Legal+ Notices displayed by works containing it; or++ c) Prohibiting misrepresentation of the origin of that material, or+ requiring that modified versions of such material be marked in+ reasonable ways as different from the original version; or++ d) Limiting the use for publicity purposes of names of licensors or+ authors of the material; or++ e) Declining to grant rights under trademark law for use of some+ trade names, trademarks, or service marks; or++ f) Requiring indemnification of licensors and authors of that+ material by anyone who conveys the material (or modified versions of+ it) with contractual assumptions of liability to the recipient, for+ any liability that these contractual assumptions directly impose on+ those licensors and authors.++ All other non-permissive additional terms are considered "further+restrictions" within the meaning of section 10. If the Program as you+received it, or any part of it, contains a notice stating that it is+governed by this License along with a term that is a further+restriction, you may remove that term. If a license document contains+a further restriction but permits relicensing or conveying under this+License, you may add to a covered work material governed by the terms+of that license document, provided that the further restriction does+not survive such relicensing or conveying.++ If you add terms to a covered work in accord with this section, you+must place, in the relevant source files, a statement of the+additional terms that apply to those files, or a notice indicating+where to find the applicable terms.++ Additional terms, permissive or non-permissive, may be stated in the+form of a separately written license, or stated as exceptions;+the above requirements apply either way.++ 8. Termination.++ You may not propagate or modify a covered work except as expressly+provided under this License. Any attempt otherwise to propagate or+modify it is void, and will automatically terminate your rights under+this License (including any patent licenses granted under the third+paragraph of section 11).++ However, if you cease all violation of this License, then your+license from a particular copyright holder is reinstated (a)+provisionally, unless and until the copyright holder explicitly and+finally terminates your license, and (b) permanently, if the copyright+holder fails to notify you of the violation by some reasonable means+prior to 60 days after the cessation.++ Moreover, your license from a particular copyright holder is+reinstated permanently if the copyright holder notifies you of the+violation by some reasonable means, this is the first time you have+received notice of violation of this License (for any work) from that+copyright holder, and you cure the violation prior to 30 days after+your receipt of the notice.++ Termination of your rights under this section does not terminate the+licenses of parties who have received copies or rights from you under+this License. If your rights have been terminated and not permanently+reinstated, you do not qualify to receive new licenses for the same+material under section 10.++ 9. Acceptance Not Required for Having Copies.++ You are not required to accept this License in order to receive or+run a copy of the Program. Ancillary propagation of a covered work+occurring solely as a consequence of using peer-to-peer transmission+to receive a copy likewise does not require acceptance. However,+nothing other than this License grants you permission to propagate or+modify any covered work. These actions infringe copyright if you do+not accept this License. Therefore, by modifying or propagating a+covered work, you indicate your acceptance of this License to do so.++ 10. Automatic Licensing of Downstream Recipients.++ Each time you convey a covered work, the recipient automatically+receives a license from the original licensors, to run, modify and+propagate that work, subject to this License. You are not responsible+for enforcing compliance by third parties with this License.++ An "entity transaction" is a transaction transferring control of an+organization, or substantially all assets of one, or subdividing an+organization, or merging organizations. If propagation of a covered+work results from an entity transaction, each party to that+transaction who receives a copy of the work also receives whatever+licenses to the work the party's predecessor in interest had or could+give under the previous paragraph, plus a right to possession of the+Corresponding Source of the work from the predecessor in interest, if+the predecessor has it or can get it with reasonable efforts.++ You may not impose any further restrictions on the exercise of the+rights granted or affirmed under this License. For example, you may+not impose a license fee, royalty, or other charge for exercise of+rights granted under this License, and you may not initiate litigation+(including a cross-claim or counterclaim in a lawsuit) alleging that+any patent claim is infringed by making, using, selling, offering for+sale, or importing the Program or any portion of it.++ 11. Patents.++ A "contributor" is a copyright holder who authorizes use under this+License of the Program or a work on which the Program is based. The+work thus licensed is called the contributor's "contributor version".++ A contributor's "essential patent claims" are all patent claims+owned or controlled by the contributor, whether already acquired or+hereafter acquired, that would be infringed by some manner, permitted+by this License, of making, using, or selling its contributor version,+but do not include claims that would be infringed only as a+consequence of further modification of the contributor version. For+purposes of this definition, "control" includes the right to grant+patent sublicenses in a manner consistent with the requirements of+this License.++ Each contributor grants you a non-exclusive, worldwide, royalty-free+patent license under the contributor's essential patent claims, to+make, use, sell, offer for sale, import and otherwise run, modify and+propagate the contents of its contributor version.++ In the following three paragraphs, a "patent license" is any express+agreement or commitment, however denominated, not to enforce a patent+(such as an express permission to practice a patent or covenant not to+sue for patent infringement). To "grant" such a patent license to a+party means to make such an agreement or commitment not to enforce a+patent against the party.++ If you convey a covered work, knowingly relying on a patent license,+and the Corresponding Source of the work is not available for anyone+to copy, free of charge and under the terms of this License, through a+publicly available network server or other readily accessible means,+then you must either (1) cause the Corresponding Source to be so+available, or (2) arrange to deprive yourself of the benefit of the+patent license for this particular work, or (3) arrange, in a manner+consistent with the requirements of this License, to extend the patent+license to downstream recipients. "Knowingly relying" means you have+actual knowledge that, but for the patent license, your conveying the+covered work in a country, or your recipient's use of the covered work+in a country, would infringe one or more identifiable patents in that+country that you have reason to believe are valid.++ If, pursuant to or in connection with a single transaction or+arrangement, you convey, or propagate by procuring conveyance of, a+covered work, and grant a patent license to some of the parties+receiving the covered work authorizing them to use, propagate, modify+or convey a specific copy of the covered work, then the patent license+you grant is automatically extended to all recipients of the covered+work and works based on it.++ A patent license is "discriminatory" if it does not include within+the scope of its coverage, prohibits the exercise of, or is+conditioned on the non-exercise of one or more of the rights that are+specifically granted under this License. You may not convey a covered+work if you are a party to an arrangement with a third party that is+in the business of distributing software, under which you make payment+to the third party based on the extent of your activity of conveying+the work, and under which the third party grants, to any of the+parties who would receive the covered work from you, a discriminatory+patent license (a) in connection with copies of the covered work+conveyed by you (or copies made from those copies), or (b) primarily+for and in connection with specific products or compilations that+contain the covered work, unless you entered into that arrangement,+or that patent license was granted, prior to 28 March 2007.++ Nothing in this License shall be construed as excluding or limiting+any implied license or other defenses to infringement that may+otherwise be available to you under applicable patent law.++ 12. No Surrender of Others' Freedom.++ If conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License. If you cannot convey a+covered work so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you may+not convey it at all. For example, if you agree to terms that obligate you+to collect a royalty for further conveying from those to whom you convey+the Program, the only way you could satisfy both those terms and this+License would be to refrain entirely from conveying the Program.++ 13. Use with the GNU Affero General Public License.++ Notwithstanding any other provision of this License, you have+permission to link or combine any covered work with a work licensed+under version 3 of the GNU Affero General Public License into a single+combined work, and to convey the resulting work. The terms of this+License will continue to apply to the part which is the covered work,+but the special requirements of the GNU Affero General Public License,+section 13, concerning interaction through a network will apply to the+combination as such.++ 14. Revised Versions of this License.++ The Free Software Foundation may publish revised and/or new versions of+the GNU General Public License from time to time. Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++ Each version is given a distinguishing version number. If the+Program specifies that a certain numbered version of the GNU General+Public License "or any later version" applies to it, you have the+option of following the terms and conditions either of that numbered+version or of any later version published by the Free Software+Foundation. If the Program does not specify a version number of the+GNU General Public License, you may choose any version ever published+by the Free Software Foundation.++ If the Program specifies that a proxy can decide which future+versions of the GNU General Public License can be used, that proxy's+public statement of acceptance of a version permanently authorizes you+to choose that version for the Program.++ Later license versions may give you additional or different+permissions. However, no additional obligations are imposed on any+author or copyright holder as a result of your choosing to follow a+later version.++ 15. Disclaimer of Warranty.++ THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY+APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM+IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.++ 16. Limitation of Liability.++ IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF+SUCH DAMAGES.++ 17. Interpretation of Sections 15 and 16.++ If the disclaimer of warranty and limitation of liability provided+above cannot be given local legal effect according to their terms,+reviewing courts shall apply local law that most closely approximates+an absolute waiver of all civil liability in connection with the+Program, unless a warranty or assumption of liability accompanies a+copy of the Program in return for a fee.++ END OF TERMS AND CONDITIONS++ How to Apply These Terms to Your New Programs++ If you develop a new program, and you want it to be of the greatest+possible use to the public, the best way to achieve this is to make it+free software which everyone can redistribute and change under these terms.++ To do so, attach the following notices to the program. It is safest+to attach them to the start of each source file to most effectively+state the exclusion of warranty; and each file should have at least+the "copyright" line and a pointer to where the full notice is found.++ {one line to give the program's name and a brief idea of what it does.}+ Copyright (C) {year} {name of author}++ This program is free software: you can redistribute it and/or modify+ it under the terms of the GNU General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ This program is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU General Public License for more details.++ You should have received a copy of the GNU General Public License+ along with this program. If not, see <http://www.gnu.org/licenses/>.++Also add information on how to contact you by electronic and paper mail.++ If the program does terminal interaction, make it output a short+notice like this when it starts in an interactive mode:++ {project} Copyright (C) {year} {fullname}+ This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+ This is free software, and you are welcome to redistribute it+ under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License. Of course, your program's commands+might be different; for a GUI interface, you would use an "about box".++ You should also get your employer (if you work as a programmer) or school,+if any, to sign a "copyright disclaimer" for the program, if necessary.+For more information on this, and how to apply and follow the GNU GPL, see+<http://www.gnu.org/licenses/>.++ The GNU General Public License does not permit incorporating your program+into proprietary programs. If your program is a subroutine library, you+may consider it more useful to permit linking proprietary applications with+the library. If this is what you want to do, use the GNU Lesser General+Public License instead of this License. But first, please read+<http://www.gnu.org/philosophy/why-not-lgpl.html>.
+ README.md view
@@ -0,0 +1,250 @@+# GenZ - A Generic Sequent Calculus Prover using the Zipper++Covering the following logics:++- Propositional: CPL, IPL+- Modal: K, K4, K45, T, D, D4, D45, S4, GL++## Web interface++You can use the prover online at <https://tools.malv.in/genz-web/>.++## Formula Syntax++Both ASCII and Unicode symbols are allowed. Here are some example formulas:++- `[](p -> []p) -> []p`+- `[]p & []q <-> []p | []q` which unfolds to `((☐p ∧ ☐q) → (☐p v ☐q)) ∧ ((☐p v ☐q) → (☐p ∧ ☐q))`.+- `<><>p -> <>p` which unfolds to `(☐((☐(p → ⊥) → ⊥) → ⊥) → ⊥) → (☐(p → ⊥) → ⊥)`++| Symbols | Meaning | Note |+|--------------------------|-------------------------|----------------------------------|+| `p`, `q`, `bla`, ... | atomic propositions | |+| `true`, ⊤ | top (constant true) | |+| `false`, ⊥ | bottom (constant false) | |+| `!`, `~`, `¬` | negation (not) | abreviation for `... -> false` |+| `&` | conjunction (and) | primitive |+| `\|`, `v` | disjunction (or) | primitive |+| `->`, `-->`, `=>`, `→`, | implication (if-then) | primitive |+| `<->`, `<-->`, `<=>`,`↔` | bi-implication (iff) | abbreviation using `->` and `&`. |+| `<>`, `<a>`, `◇` | diamond (possible) | abbreviation for `~ [] ~ ...` |+| `[]`, `[a]`, `☐`, `◻` | box (necessary) | primitive |++## Building++You should have the Haskell build tool `stack` installed, via [ghcup](https://www.haskell.org/ghcup/).+For proof visualization, optonally you may want to install [`graphviz`](https://graphviz.org/).++To build the project run `stack build`.++## CLI program++To install the `genz` and the `genz-web` binaries, just run `stack install` in this repository.++### CLI examples++We can prove a formula given directly with `-F` or from a file with `-f` or from standard input with `--stdin`.+By default the modal logic `K` is used.++```+$ genz -F "[]p -> [][]p"+False++$ echo "p | ~p" > example.txt+$ genz -f example.txt+True+$ genz -f example.txt --logic IPL+False++$ echo "[][]p -> [][][][]p" | genz --stdin --logic S4+True+```++Get help:++```+$ genz --help+genz - a generic sequent calculus prover with zippers++Usage: genz ((-F|--formula FORMULA) | (-f|--file FILE) | (-s|--stdin))+ [-i|--input INPUT] [-t|--tree] [-n|--negate] [-d|--debug]+ [-p|--proofFormat FORMAT] [-l|--logic LOGIC]++ Prove the given FORMULA or the formula in FILE or STDIN.++Available options:+ -F,--formula FORMULA Formula+ -f,--file FILE Input file+ -s,--stdin Read from stdin+ -i,--input INPUT Input format: single, tptp (default: single)+ -t,--tree Use standard trees (default is to use zippers).+ -n,--negate Negate the input formula.+ -d,--debug Print additional debug information.+ -p,--proofFormat FORMAT Proof format: none, plain, buss, size (default: none)+ -l,--logic LOGIC Logic to use: CPL, IPL, D, D4, D45, GL, K, K4, K45,+ S4, T (default: K)+ -h,--help Show this help text+```++Benchmarking zipper vs tree representation (for an unprovable formula):+```+$ /usr/bin/time -f%E genz -F "[]([]p->p) -> [][][][][][][][][][][][][][][][][][]p" --logic K4+False+0:00.01+$ /usr/bin/time -f%E genz -F "[]([]p->p) -> [][][][][][][][][][][][][][][][][][]p" --logic K4 --tree+False+0:03.44+```++## Haskell examples++You can use `stack ghci` to run examples like this:++ stack ghci lib/Logic/Modal/K.hs lib/FormM.hs++ ghci> FormM.multiVerK 3+ (☐(3 → (4 → (5 → 1))) → (☐3 → (☐4 → (☐5 → ☐1))))+ ghci> FormM.extraAtK 3+ (☐(3 → (4 → (5 → (2 → 1)))) → (☐3 → (☐4 → (☐5 → ☐1))))++ ghci> isProvableT k (FormM.multiVerK 3)+ True+ ghci> isProvableZ k (FormM.multiVerK 3)+ True+ ghci> isProvableT k (FormM.extraAtK 3)+ False+ ghci> isProvableZ k (FormM.extraAtK 3)+ False++In the above `k` is `Logic.Modal.K.k :: Logic`, i.e. the proof system.++## Defining Your Own Logic++A `Logic` in GenZ is a collection of **safeRules** (invertible, applied greedily) and **unsafeRules** (non-invertible, requiring backtracking and possibly loopchecks):+```haskell+data Logic f = Log { name :: String+ , safeRules :: [Rule f]+ , unsafeRules :: [Rule f] }+```++Each rule takes a history, the current sequent, and a principal formula, and returns possibly multiple branches:+```haskell+type Rule f = History f -> Sequent f -> Either f f -> [(RuleName, [Sequent f])]+```++As an example, CPL has only safe rules:+```haskell+classical :: Logic FormP+classical = Log { name = "CPL"+ , safeRules = [leftBot, isAxiom, replaceRule safeCPL]+ , unsafeRules = []+ }++safeCPL :: Either FormP FormP -> [(RuleName,[Sequent FormP])]+safeCPL (Left (ConP f g)) = [("∧L", [Set.fromList [Left g, Left f]])]+safeCPL (Left (DisP f g)) = [("vL", [Set.singleton (Left f), Set.singleton (Left g)])]+safeCPL (Left (ImpP f g)) = [("→L", [Set.singleton (Right f), Set.singleton (Left g)])]+safeCPL (Right (ConP f g)) = [("∧R", [Set.singleton (Right f), Set.singleton (Right g)])]+safeCPL (Right (DisP f g)) = [("vR", [Set.fromList [Right g, Right f]])]+safeCPL (Right (ImpP f g)) = [("→R", [Set.fromList [Right g, Left f]])]+safeCPL _ = []+```++For logics that require backtracking (e.g. IPL, modal logics), place non-invertible rules in `unsafeRules`. See `lib/Logic/` for all implemented calculi.+Implementation for loopchecks can be found in `lib/Logic/Propositional/IPL.hs` for reference.++To try your own logic, create a new module under `lib/Logic/`, following the structure above. Then load it in ghci. Below is an example of a modal logic. You can also define your own language and your own formula examples.+```+$ stack ghci lib/General.hs lib/FormM.hs lib/Logic/YourLogic.hs+ghci> isProvableZ yourLogic (ImpM (AtM '1') (AtM '1'))+True+```++## LaTeX output++The prover can generate code for [bussproofs](https://ctan.org/pkg/bussproofs).++For example++ stack exec genz -- -F "□(□p → p) → □p" -l GL -p buss++will print the LaTeX code for the following proof:++++When using *ghci* instead of the `genz` executable, the following+command can be used to write the code into `temp.tex` and then run+`pdflatex` on it directly:++ stack ghci lib/Logic/Modal/GL.hs lib/FormM.hs++ ghci> texFile . head . proveZ gl $ ImpM (Box (ImpM (Box (AtM "p")) (AtM "p"))) (Box (AtM "p"))++## The Zipper Data Structure++GenZ uses the **zipper**, a data structure introduced by [Huet (1997)](https://doi.org/10.1017/S0956796897002864), to efficiently navigate and modify proof trees during proof search. The idea is to split a tree into a **focus** (the subtree being worked on) and a **path** (everything above and around it), enabling constant-time navigation and modification without reconstructing the entire tree.++A standard tree and its zipper in Haskell:+```haskell+data Tree a = Node a [Tree a]+data ZipTree a = ZT (Tree a) (Path a)+data Path a = Top | Step a (Path a) [Tree a] [Tree a]+```++A `ZipTree` focuses on a subtree, while `Path` records the parent node, the path further up, and the left/right siblings. For example, in this tree with focus at node `2`:+```+ 0+ / | \ \+ 1 [2] 3 4+ | / \+ 5 6 7++ZT (Node 2 [Node 5 []])+ (Step 0 Top [Node 1 []] [Node 3 [], Node 4 [Node 6 [], Node 7 []]])+```++GenZ applies this to proof search trees via `ZipProof` and `ZipPath`:+```haskell+data ZipProof f = ZP (Proof f) (ZipPath f)+data ZipPath f = Top | Step (Sequent f) RuleName (ZipPath f) [Proof f] [Proof f]+```++This makes backtracking efficient: when a rule application fails, GenZ moves the focus back up and tries a different rule without rebuilding the tree.++## Tests++To run all tests locally, run `stack test`.+This should not take more than five minutes.++The tests are also run automatically for each commit,+see <https://github.com/XiaoshuangYang999/GenZ/actions> for results.++## LWB and ILTP Benchmarks++See the `benchmarks` folder for bash scripts to run GenZ on these benchmarks.++## Custom Benchmarks (`bench` folder)++You should have LaTeX and [pandoc](https://pandoc.org/) installed.++To run the benchmarks for a small selection of formulas,+run `make bench/runtime.pdf` and `make bench/memory.pdf`.+The runtime benchmark will take around 30 minutes, the memory benchmark less than one minute.++To run benchmarks on a larger set of formulas,+run `make bench/runtime-all.pdf` and `make bench/memory-all.pdf`.+Note: this runtime benchmark will take multiple hours.++Example results are available at+<https://github.com/XiaoshuangYang999/GenZ/releases>.++## References++The code in this repository was originally developed as part of the following master's thesis:++- Xiaoshuang Yang: *Sequent Calculus with Zippers*.+ University of Amsterdam, 2024.+ <https://eprints.illc.uva.nl/id/eprint/2354>++The original code from the thesis can be found in the `thesis-version` branch.+Ongoing updates and improvements are included in the `main` branch.
+ bench/memory.hs view
@@ -0,0 +1,46 @@+module Main (main) where++import System.Environment (getArgs)+import Data.List+import Weigh+import General+import Logic.Propositional.CPL+import Logic.Propositional.IPL+import Logic.Modal.K+import Logic.Modal.K4+import Logic.Modal.GL+import Logic.Modal.S4+import FormM+import FormP++main :: IO ()+main = do+ args <- getArgs+ mainWith $+ if "--all-formulas" `elem` args+ then do+ -- all formulas:+ makeCases [ ("CPL", classical), ("IPL", intui) ] allFormulasP [100]+ makeCases [ ("K", k), ("K4", kfour), ("GL", gl), ("S4", sfour) ] propFormulasM [10]+ makeCases [ ("K", k), ("K4", kfour), ("GL", gl), ("S4", sfour) ] boxesFormulasM [10]+ makeCases [ ("K", k) ] kFormulasM [2]+ makeCases [ ("K4", kfour) ] k4FormulasM [2]+ makeCases [ ("GL", gl) ] glFormulasM [2]+ makeCases [ ("S4", sfour) ] s4FormulasM [5]+ else do+ -- selected four formulas:+ makeCases [ ("IPL", intui) ] [("conPeiL",conPeiL), ("conPeiR",conPeiR)] [100] -- not provable+ makeCases [ ("K", k) ] [("boxesTop",boxesTop)] [1000] -- provable+ makeCases [ ("K4", kfour) ] [("lobBoxes",lobBoxes)] [10] -- not provable+ makeCases [ ("GL", gl) ] [("lobBoxes",lobBoxes)] [100] -- provable++makeCases :: (Ord f, Show f) => [(String, Logic f)] -> [(String, Int -> f)] -> [Int] -> Weigh ()+makeCases logics forms sizes = mapM_ (\ (label, logic, method, form, n) -> func label (method logic . form) n)+ [ (intercalate "|" [logicStr, formStr, methodStr, show n, show result], logic, method, formFor, n)+ | (logicStr, logic) <- logics+ , (formStr, formFor) <- forms+ , (methodStr, method) <- [ ("GenT", isProvableT)+ , ("GenZ ", isProvableZ) ]+ , n <- sizes+ , let result = method logic (formFor n)+ ]
+ bench/runtime.hs view
@@ -0,0 +1,126 @@+module Main where++import Control.Monad (unless, when)+import Criterion.Main+import qualified Criterion.Types+import qualified Data.ByteString.Lazy as BL+import Data.Char (isSpace)+import Data.Csv+import Data.List+import Data.List.Split+import Data.Maybe+import Data.Scientific+import qualified Data.Vector as V+import Numeric+import System.Directory+import System.Environment (getArgs)+import General+import Logic.Propositional.CPL+import Logic.Propositional.IPL+import Logic.Modal.K+import Logic.Modal.K4+import Logic.Modal.GL+import Logic.Modal.S4+import FormM+import FormP++type Case = (String, Int -> Bool, [Int])++-- | Selected formulas. Takes only a few minutes to run.+selection :: [Case]+selection =+ makeCases [ ("IPL", intui) ] [("conPei-L", conPeiL), ("conPei-R", conPeiR)] [10,20..100] -- not provable+ ++ makeCases [ ("K", k) ] [("boxesTop", boxesTop)] [10,20..100] -- provable+ ++ makeCases [ ("K4", kfour) ] [("lobBoxes", lobBoxes)] [1..10] -- not provable+ ++ makeCases [ ("GL", gl) ] [("lobBoxes", lobBoxes)] [1..10] -- provable++-- | Large set of formulas. Can take multple hours to run.+allFormulas :: [Case]+allFormulas =+ makeCases [("CPL", classical), ("IPL", intui) ] allFormulasP [10,20..100]+ ++ makeCases [("CPL", classical), ("IPL", intui) ] hardFormulasP [1..10]+ ++ makeCases [("K", k)] (propFormulasM ++ boxesFormulasM) [10,20..100]+ ++ makeCases [("K", k)] kFormulasM [1..10]+ ++ makeCases [("K4", kfour)] (propFormulasM ++ boxesFormulasM) [10,20..100]+ ++ makeCases [("K4", kfour)] k4FormulasM [1..8]+ ++ makeCases [("GL", gl)] propFormulasM [10,20..100]+ ++ makeCases [("S4", sfour)] propFormulasM [10,20..100]+ ++ makeCases [("S4", sfour)] hards4FormulasM [1..10]++-- | Helper function to run the maximum size of each case.+-- Ueful to adjust the ranges given above.+testAllMaxSizeItems :: IO ()+testAllMaxSizeItems = mapM_ func allItems where+ func (n1, f, range) = do+ print (n1 ++ show (maximum range))+ print $ f (maximum range)++allItems :: [Case]+allItems = nubBy sameC $ selection ++ allFormulas where+ sameC (n1, _, _) (n2, _, _) = n1 == n2++makeCases :: (Ord f, Show f) => [(String, Logic f)] -> [(String, Int -> f)] -> [Int] -> [Case]+makeCases logics forms sizes =+ [ (fS ++ "-" ++ lS ++ "-" ++ pS , prover logic . formula, sizes)+ | (fS, formula) <- forms+ , (pS, prover) <- [("GenZ", isProvableZ), ("GenT", isProvableT)]+ , (lS, logic) <- logics ]++benchMain :: IO ()+benchMain =+ defaultMainWith myConfig (map mybench allItems) where+ mybench (name1,f,range) = bgroup name1 $ map (run f) range+ run f n = bench (show n) $ whnf f n+ myConfig = defaultConfig+ { Criterion.Types.csvFile = Just theCSVname+ , Criterion.Types.timeLimit = 10 }++main :: IO ()+main = do+ args <- getArgs+ unless ("--list" `elem` args) prepareMain+ benchMain+ unless ("--list" `elem` args) convertMain++-- * CSV to pgfplots++-- | The filename to which the benchmark results will be written in CSV.+theCSVname :: String+theCSVname = "bench/results.csv"++prepareMain :: IO ()+prepareMain = do+ oldResults <- doesFileExist theCSVname+ when oldResults $ do+ putStrLn "Note: moving away old results."+ renameFile theCSVname (theCSVname ++ ".OLD")+ oldDATfile <- doesFileExist (theCSVname ++ ".dat")+ when oldDATfile $ removeFile (theCSVname ++ ".dat")++-- | Convert the .csv file to a .dat file to be used with pgfplots.+convertMain :: IO ()+convertMain = do+ putStrLn "Reading results.csv and converting to .dat for pgfplots."+ c <- BL.readFile theCSVname+ case decode NoHeader c of+ Left err -> error $ "could not parse the csv file:" ++ show err+ Right csv -> do+ let results = map (parseLine . take 2) $ tail $ V.toList (csv :: V.Vector [String])+ let columns = nub.sort $ map (fst.fst) results+ let widthNeeded = maximum $ map length columns+ let longify = longifyTo (widthNeeded + 2)+ let firstLine = longifyTo 5 "n" ++ dropWhileEnd isSpace (concatMap longify columns)+ let resAt n col = longify $ fromMaybe "nan" $ Data.List.lookup (col,n) results+ let resultrow n = concatMap (resAt n) columns+ let firstcol = nub.sort $ map (snd.fst) results+ let resultrows = map (\n -> longifyTo 5 (show n) ++ dropWhileEnd isSpace (resultrow n)) firstcol+ writeFile (theCSVname ++ ".dat") (intercalate "\n" (firstLine:resultrows) ++ "\n")+ where+ parseLine [namestr,numberstr] = case splitOn "/" namestr of+ [name1,nstr] -> ((name1,n),valuestr) where+ n = read nstr :: Integer+ value = toRealFloat (read numberstr :: Scientific) :: Double+ valuestr = Numeric.showFFloat (Just 7) value ""+ _ -> error $ "could not parse this case: " ++ namestr+ parseLine l = error $ "could not parse this line:\n " ++ show l+ longifyTo n s = s ++ replicate (n - length s) ' '
+ exec/form-size.hs view
@@ -0,0 +1,17 @@+module Main where++import General+import General.Lex+import FormM.Parse++-- | Compute the size of lwb formulas (with extra negation)+main :: IO ()+main = do+ putStrLn "Give me the filepath: "+ p <- getLine+ content <- readFile p+ -- benchmarks/LWB/lwb_k/k_branch_n.txt.1.intohylo+ case parseFormM (alexScanTokens content) of+ Left e -> print e+ Right f -> do+ print $ size $ neg f
+ exec/genz-web.hs view
@@ -0,0 +1,118 @@+{-# LANGUAGE OverloadedStrings, TemplateHaskell #-}++module Main (main) where++import Prelude+import Data.FileEmbed+import Data.Maybe+import Web.Scotty+import qualified Data.Text as T+import qualified Data.Text.Encoding as E+import qualified Data.Text.Lazy as TL+import qualified Language.Javascript.JQuery as JQuery+import Language.Haskell.TH.Syntax+import Network.Wai.Handler.Warp (defaultSettings, setHost, setPort)+import System.Environment (lookupEnv)+import Text.Read (readMaybe)++import General+import FormP+import FormM+import General.Lex+import FormM.Parse (parseFormM)+import FormP.Parse (parseFormP)++import qualified Logic.Propositional.CPL as CPL+import qualified Logic.Propositional.IPL as IPL+import qualified Logic.Modal.D as D+import qualified Logic.Modal.D4 as D4+import qualified Logic.Modal.D45 as D45+import qualified Logic.Modal.GL as GL+import qualified Logic.Modal.K as K+import qualified Logic.Modal.K4 as K4+import qualified Logic.Modal.K45 as K45+import qualified Logic.Modal.S4 as S4+import qualified Logic.Modal.T as T++main :: IO ()+main = do+ putStrLn "GenZ web"+ port <- fromMaybe 3300 . (readMaybe =<<) <$> lookupEnv "PORT"+ path <- fromMaybe "/" <$> lookupEnv "WEBPATH"+ putStrLn $ "Please open this link: http://127.0.0.1:" ++ show port ++ path+ let mySettings = Options 1 (setHost "127.0.0.1" $ setPort port defaultSettings)+ let index = html . TL.fromStrict $ embeddedFile "index.html"+ scottyOpts mySettings $ do+ get (capture path) index+ get (capture $ path ++ "index.html") index+ get (capture $ path ++ "jquery.js") . (\t -> addHeader "Content-Type" "text/javascript" >> html t) . TL.fromStrict $ embeddedFile "jquery.js"+ post (capture $ path ++ "prove") $ do+ textinput <- param "textinput"+ let lexResult = alexScanTokensSafe textinput+ output <- case lexResult of+ Left (_,col) -> return+ [ "<pre>INPUT: " ++ textinput ++ "</pre>"+ , "<pre>" ++ replicate (col + length ("INPUT:" :: String)) ' ' ++ "^</pre>"+ , "<pre>Lexing error in column " ++ show col ++ ".</pre>" ]+ Right tokenList -> do+ useProp <- (== ("prop" :: String)) <$> param "syntax"+ s_logic <- param "logic"+ s_struct <- param "struct"+ let myParserLogic = if useProp+ then (fmap Left . parseFormP, Left (propLogic s_logic))+ else (fmap Right . parseFormM, Right (modLogic s_logic))+ case fst myParserLogic tokenList of+ Left (_,col) ->+ return+ [ "<pre>INPUT: " ++ textinput ++ "</pre>"+ , "<pre>" ++ replicate (col + length ("INPUT:" :: String)) ' ' ++ "^</pre>"+ , "<pre>Parse error in column " ++ show col ++ ".</pre>" ]+ Right lr_frm ->+ return $ webProveWrap (snd myParserLogic) lr_frm s_struct+ html $ mconcat $ map TL.pack output++propLogic :: String -> Logic FormP+propLogic s = case s of "CPL" -> CPL.classical+ "IPL" -> IPL.intui+ _ -> error $ "Unknown propositional logic: " ++ s++modLogic :: String -> Logic FormM+modLogic s = case s of+ "D" -> D.d+ "D4" -> D4.dfour+ "D45"-> D45.dfourfive+ "GL" -> GL.gl+ "K" -> K.k+ "K4" -> K4.kfour+ "K45" -> K45.kfourfive+ "S4" -> S4.sfour+ "T" -> T.t+ _ -> error $ "Unknown modal logic: " ++ s++webProveWrap :: Either (Logic FormP) (Logic FormM) -> Either FormP FormM -> String -> [String]+webProveWrap (Left l) (Left f) = webProve l f+webProveWrap (Right l) (Right f) = webProve l f+webProveWrap _ _ = error "Wrong combination of logic and syntax."++webProve :: (Eq f, Ord f, Show f, TeX f) => Logic f -> f -> String -> [String]+webProve logic frm struct =+ let (isPrv, prv) = case struct of+ "zipper" -> (isProvableZ, proofZ)+ "tree" -> (isProvableT, proofT)+ _ -> error $ "Unknown data structure: " ++ struct+ p_tex = case prv logic frm of+ Nothing -> ""+ Just p1 -> tex p1+ in+ [ "<pre>Parsed input: " ++ show frm ++ "</pre>" -- TODO pretty? tex?+ , if isPrv logic frm+ then "PROVED. <style type='text/css'> #output { border-color: green; } </style>\n"+ else "NOT proved. <style type='text/css'> #output { border-color: red; } </style>\n"+ , if p_tex /= "" then "<div align='center'>\\( \\begin{prooftree}" ++ p_tex ++ " \\end{prooftree} \\)</div>" else ""+ ]++embeddedFile :: String -> T.Text+embeddedFile str = case str of+ "index.html" -> E.decodeUtf8 $(embedFile "exec/index.html")+ "jquery.js" -> E.decodeUtf8 $(embedFile =<< runIO JQuery.file)+ _ -> error "File not found."
+ exec/genz.hs view
@@ -0,0 +1,194 @@+{-# LANGUAGE LambdaCase #-}++module Main where++import Options.Applicative+import Data.Maybe++import General+import General.Lex+import General.Token++import FormP+import FormM+import FormM.Parse+import FormP.Parse+import FormP.ParseTPTP++import qualified Logic.Propositional.CPL as CPL+import qualified Logic.Propositional.IPL as IPL+import qualified Logic.Modal.D as D+import qualified Logic.Modal.D4 as D4+import qualified Logic.Modal.D45 as D45+import qualified Logic.Modal.GL as GL+import qualified Logic.Modal.K as K+import qualified Logic.Modal.K4 as K4+import qualified Logic.Modal.K45 as K45+import qualified Logic.Modal.S4 as S4+import qualified Logic.Modal.T as T++data Input = FileInput FilePath | DirectInput String | StdInput++data InputFormat = InSingle | InTPTP++data Config = Config+ { input :: Input+ , inFormat :: InputFormat+ , tree :: Bool+ , negate :: Bool+ , debug :: Bool+ , proof :: ProofFormat+ , log :: MyLogic }++main :: IO ()+main = runGenZ =<< execParser opts where+ opts = info (configP <**> helper) (fullDesc <> progDesc "Prove the given FORMULA or the formula in FILE or STDIN."+ <> header "genz - a generic sequent calculus prover with zippers")++runGenZ :: Config -> IO ()+runGenZ (Config inp inf useTree negIn deb prFormat myL) = do+ form_in <- case inp of FileInput file -> readFile file -- TODO: ignore "begin" and "end" here or in Lexer/Parser?+ DirectInput f_s -> return f_s+ StdInput -> getContents -- TODO same++ let form_s = case inf of InSingle -> form_in+ InTPTP -> case rewriteTPTPProblem form_in of Left _ -> error "Could not parse TPTP file"+ Right fs -> fs++ let tl = case myLex form_s of Left errs -> error $ unlines errs+ Right tl_ -> tl_+ putStrLn $ case myL of+ Left l_prop ->+ case myParse form_s tl parseFormP of+ Left errs -> error (unlines errs)+ Right f_prop ->+ (if deb then "Tree size of formula: " ++ show (size $ neg f_prop) ++ "\n" else "") +++ prChoose useTree prFormat l_prop ((if negIn then neg else id) f_prop)+ Right l_mod ->+ case myParse form_s tl parseFormM of+ Left errs -> error (unlines errs)+ Right f_mod ->+ (if deb then "Tree size of formula: " ++ show (size $ neg f_mod) ++ "\n" else "") +++ prChoose useTree prFormat l_mod ((if negIn then neg else id) f_mod)++-- | Helper to chooe tree/zipper and bool/proof output+prChoose :: (Show f, Ord f, TeX f) => Bool -> ProofFormat -> Logic f -> (f -> String)+prChoose True None l = show . isProvableT l+prChoose True Plain l = ppProof . fromJust . proofT l+prChoose True Buss l = tex . fromJust . proofT l+prChoose True Size l = show . proofSize . fromJust . proofT l+prChoose False None l = show . isProvableZ l+prChoose False Plain l = ppProof . fromJust . proofZ l+prChoose False Buss l = tex . fromJust . proofZ l+prChoose False Size l = show . proofSize . fromJust . proofZ l++configP :: Parser Config+configP = Config+ <$> inputP+ <*> option (maybeReader inputFormatR)+ ( long "input"+ <> short 'i'+ <> help "Input format: single, tptp"+ <> showDefaultWith ppInputFormat+ <> value InSingle+ <> metavar "INPUT" )+ <*> Options.Applicative.switch+ ( long "tree"+ <> short 't'+ <> help "Use standard trees (default is to use zippers)." )+ <*> Options.Applicative.switch+ ( long "negate"+ <> short 'n'+ <> help "Negate the input formula." )+ <*> Options.Applicative.switch+ ( long "debug"+ <> short 'd'+ <> help "Print additional debug information." )+ <*> option (maybeReader outputR)+ ( long "proofFormat"+ <> short 'p'+ <> help "Proof format: none, plain, buss, size"+ <> showDefaultWith ppProofFormat+ <> value None+ <> metavar "FORMAT" )+ <*> option (maybeReader logicR)+ ( long "logic"+ <> short 'l'+ <> help "Logic to use: CPL, IPL, D, D4, D45, GL, K, K4, K45, S4, T"+ <> showDefaultWith (\ case Left l -> name l; Right l -> name l)+ <> value (Right K.k)+ <> metavar "LOGIC" )++ppInputFormat :: InputFormat -> String+ppInputFormat InSingle = "single"+ppInputFormat InTPTP = "tptp"++inputFormatR :: String -> Maybe InputFormat+inputFormatR i_s = case i_s of+ "single" -> return InSingle+ "tptp" -> return InTPTP+ "TPTP" -> return InTPTP+ _ -> error $ "Unknown input format: " ++ i_s++data ProofFormat = None | Plain | Buss | Size++ppProofFormat :: ProofFormat -> String+ppProofFormat None = "none"+ppProofFormat Plain = "plain"+ppProofFormat Buss = "buss"+ppProofFormat Size = "size"++outputR :: String -> Maybe ProofFormat+outputR o_s = case o_s of+ "none" -> return None+ "plain" -> return Plain+ "buss" -> return Buss+ "size" -> return Size+ _ -> error $ "Unknown output format: " ++ o_s++type MyLogic = (Either (Logic FormP) (Logic FormM))++logicR :: String -> Maybe MyLogic+logicR l_s = case l_s of+ "CPL" -> return $ Left CPL.classical+ "IPL" -> return $ Left IPL.intui+ "D" -> return $ Right D.d+ "D4" -> return $ Right D4.dfour+ "D45" -> return $ Right D45.dfourfive+ "GL" -> return $ Right GL.gl+ "K" -> return $ Right K.k+ "K4" -> return $ Right K4.kfour+ "K45" -> return $ Right K45.kfourfive+ "S4" -> return $ Right S4.sfour+ "T" -> return $ Right T.t+ _ -> error $ "Unknown logic: " ++ l_s++fileInputP :: Parser Input+fileInputP = FileInput <$> strOption (long "file" <> short 'f' <> metavar "FILE" <> help "Input file" )++directInputP :: Parser Input+directInputP = DirectInput <$> strOption (long "formula" <> short 'F' <> metavar "FORMULA" <> help "Formula" )++stdInputP :: Parser Input+stdInputP = flag' StdInput (long "stdin" <> short 's' <> help "Read from stdin" )++inputP :: Parser Input+inputP = directInputP <|> fileInputP <|> stdInputP++myLex :: String -> Either [String] [Token AlexPosn]+myLex textinput = do+ let lexResult = alexScanTokensSafe textinput+ case lexResult of+ Left (line,col) -> Left+ [ "\nINPUT: " ++ textinput+ , replicate (col + length ("INPUT:" :: String)) ' ' ++ "^"+ , "Lexing error in line " ++ show line ++ " column " ++ show col ++ "." ]+ Right tokenList -> Right tokenList++myParse :: String -> [Token AlexPosn] -> ([Token AlexPosn] -> Either (Int,Int) f) -> Either [String] f+myParse textinput tl myParser = case myParser tl of+ Left (line,col) -> Left+ [ "\nINPUT: " ++ textinput+ , replicate (col + length ("INPUT:" :: String)) ' ' ++ "^"+ , "Parse error in line " ++ show line ++ " column " ++ show col ]+ Right frm -> Right frm
+ exec/index.html view
@@ -0,0 +1,248 @@+<!DOCTYPE html>+<html lang="en">+ <head>+ <title>GenZ prover</title>+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />+ <meta name="viewport" content="width=device-width, minimum-scale=1.0, maximum-scale=1.0" />+ <script src="jquery.js"></script>+ <script>+ MathJax = {+ tex: {+ inlineMath: {'[+]': [['$', '$']]}+ }+ };+ </script>+ <script defer src="https://cdn.jsdelivr.net/npm/mathjax@4/tex-chtml.js"></script>+ <style type="text/css">+ #textinput {+ font-size:110%;+ margin: 0.1em;+ padding: 0.1em;+ width:50%;+ }+ #help {+ border:1px solid gray;+ display:none;+ margin-bottom:1em;+ }+ #help pre {+ font-size:120%;+ }+ #runbutton {+ font-size:110%;+ width:40%;+ }+ #output {+ border: 2px solid #666;+ margin-top: 1em;+ padding: 1em;+ width:auto;+ overflow-x: hidden;+ }+ pre, svg {+ overflow-x: auto;+ max-width:100%;+ height:auto;+ }+ .success {+ color: green;+ }+ .error {+ color: red;+ font-weight:bold;+ }+ #running {+ color: orange;+ display: none;+ float: right;+ }+ details {+ margin-top:1em;+ border: 1px solid #ddd;+ border-radius:2px;+ padding-left:5px;+ }+ summary h3 {+ display:inline;+ }+ .linker {+ color:gray;+ float:right;+ cursor:pointer;+ }+ .linker:active {+ color: black;+ text-shadow: 1px 2px #666;+ transform: translateY(2px) translateX(2px);+ }++ /* responsiveness */+ @media screen and (max-width: 600px) {+ #textinput { width:97% !important; }+ #runbutton { width:100%; }+ }++ </style>+ <link rel="icon" href="data:,">+ </head>+ <body>+ <p>+ This is the web interface of+ <a href="https://github.com/XiaoshuangYang999/GenZ">GenZ</a>.+ </p>+ <p>+ Please choose+ <label for="logic">a logic:</label>+ <select name="logic" id="logic">+ <optgroup label="Propositional">+ <option value="prop">CPL</option>+ <option value="prop">IPL</option>+ </optgroup>+ <optgroup label="Modal">+ <option value="modal">D</option>+ <option value="modal">D4</option>+ <option value="modal">D45</option>+ <option value="modal">GL</option>+ <option value="modal" selected>K</option>+ <option value="modal">K4</option>+ <option value="modal">K45</option>+ <option value="modal">S4</option>+ <option value="modal">T</option>+ </optgroup>+ </select>+ and a+ <label for="struct">data structure:</label>+ <select name="struct" id="struct">+ <option value="zipper">zipper</option>+ <option value="tree">tree</option>+ </select>+ </p>+ <p>+ Enter a formula below <a href="#" onClick='$("#help").slideToggle()'>using this syntax</a> or <label for="examples">choose an example:</label>+ <select name="examples" id="examples">+ <optgroup label="CPL">+ <option value="CPL">p → p</option>+ <option value="CPL">p → ¬¬p</option>+ <option value="CPL">p ↔ ¬¬p</option>+ </optgroup>+ <optgroup label="IPL">+ <option value="IPL">p → p</option>+ <option value="IPL">p → ¬¬p</option>+ <option value="IPL">p ↔ ¬¬p</option>+ <option value="IPL">¬¬(p | ¬p)</option>+ <option value="IPL">(p → q) → ⊥</option><!-- not valid -->+ </optgroup>+ <optgroup label="D">+ <option value="D">☐p → ◇p</option>+ </optgroup>+ <optgroup label="D4">+ <option value="D4">☐p → ☐☐◇p</option>+ </optgroup>+ <optgroup label="D45">+ <option value="D45">◇p → □◇p</option>+ </optgroup>+ <optgroup label="GL">+ <option value="GL">☐(☐p → p) → ☐p</option>+ </optgroup>+ <optgroup label="K">+ <option value="K" selected>☐(p1 & p2) → (☐p1 | ☐p2)</option>+ <option value="K">¬◇false</option>+ <option value="K">☐☐☐☐true</option>+ <option value="K">¬¬¬¬false</option><!-- not valid -->+ <option value="K">☐p1 → ☐☐p1</option><!-- not valid -->+ </optgroup>+ <optgroup label="K4">+ <option value="K4">☐☐p → ☐p</option>+ <option value="K4">☐☐☐☐☐☐p → ☐☐☐p</option>+ <option value="K4">◇□p | □◇□p</option><!-- not valid -->+ </optgroup>+ <optgroup label="S4">+ <option value="S4">☐☐p → ☐p</option>+ <option value="S4">p → ◇p</option>+ <option value="S4">☐(☐p → ⊥) → ☐(p → ⊥)</option><!-- not valid -->+ <option value="S4">☐(☐p → ⊥) → ☐q</option><!-- not valid -->+ </optgroup>+ <optgroup label="K45">+ <option value="K45">◇p → □◇p</option>+ </optgroup>+ <optgroup label="S4">+ <option value="S4">□□p → □p</option>+ <option value="S4">□p → □□p</option>+ </optgroup>+ <optgroup label="T">+ <option value="T">□p → p</option>+ <option value="T">p → □p</option><!-- not valid -->+ </optgroup>+ </select>+ </p>+ <div id="help">+<pre>+| Symbols | Meaning | Note |+|--------------------|-------------------------|----------------------------------|+| p, q, bla, ... | atomic propositions | |+| true, ⊤ | top (constant true) | |+| false, ⊥ | bottom (constant false) | |+| !, ~, ¬ | negation (not) | abreviation for ... -> false |+| & | conjunction (and) | primitive |+| |, v | disjunction (or) | primitive |+| ->, -->, =>, → | implication (if-then) | primitive |+| <->, <-->, <=>, ↔ | bi-implication (iff) | abbreviation using -> and & |+| <>, <a>, ◇ | diamond (possible) | abbreviation for ~ [] ~ ... |+| [], [a], ☐, ◻ | box (necessary) | primitive |+</pre>+ </div>+ <div>+ <input id="textinput" name="textinput" value="☐(p1 & p2) → (☐p1 | ☐p2)" />+ <input id="runbutton" type="submit" value="Try to prove this!" onclick="prove()" />+ <div id="running">running</div>+ </div>+ <div id="output"></div>+ <script>+ "use strict";+ function prove() {+ $('#running').css("display", "block");+ $.ajax({+ type: "POST",+ url: "prove",+ data: { "syntax": $('#logic').val()+ , "logic": $('#logic option:selected').text()+ , "textinput": $('#textinput').val()+ , "struct": $('#struct').val()+ },+ success:+ function(data,textStatus,jqXHR) {+ $('#output').html(data);+ $('#running').css("display", "none");+ MathJax.typesetPromise();+ },+ timeout: 7000,+ error:+ function(jqXHR,textStatus,errorThrown) {+ $('#output').html("<pre>" + textStatus + " " + errorThrown + "</pre>" );+ $('#running').css("display", "none");+ }+ });+ }+ $('#textinput').on('keypress', function (e) {+ if(e.which === 13){+ prove();+ }+ });+ $('#examples').change(function (e) {+ $('#textinput').val( $('#examples option:selected').text() );+ // also adjust chosen logic to the example+ $('#logic option').filter(function(index) {+ return $(this).text() === $('#examples option:selected').val();+ }).prop('selected', true);+ prove();+ });+ const hash = window.location.hash.substring(1);+ if (hash) {+ $('#textinput').val(decodeURIComponent(hash));+ $('#runbutton').click();+ // remove hash?+ // history.pushState("", document.title, window.location.pathname + window.location.search);+ }+ </script>+ </body>+</html>
+ exec/tptp-size.hs view
@@ -0,0 +1,15 @@+module Main where++import General+import FormP.ParseTPTP++-- | Compute the size of tptp formulas+main :: IO ()+main = do+ putStrLn "Give me the filepath: "+ p <- getLine+ content <- readFile p+ case parseTPTPProblem content of+ Left e -> print e+ Right f -> do+ print $ size f
+ lib/Basics.hs view
@@ -0,0 +1,75 @@+module Basics where++import Data.GraphViz+import Data.GraphViz.Types.Monadic hiding ((-->))+import GHC.IO.Handle+import System.IO+import System.IO.Temp+import System.IO.Unsafe+import qualified Data.ByteString as BS+import Data.Either+import Data.List (filter)+import Data.Set+import qualified Data.Set as Set++-- | Displayable things, using graphviz.+class DispAble t where+ toGraph :: t -> DotM String ()+ disp :: t -> IO ()+ disp x = runGraphvizCanvas Dot (digraph' $ toGraph x) Xlib+ dot :: t -> IO ()+ dot x = graphvizWithHandle Dot (digraph' $ toGraph x) Canon $ \h -> do+ hSetEncoding h utf8+ BS.hGetContents h >>= BS.putStr+ svg :: t -> String+ svg x = unsafePerformIO $ withSystemTempDirectory "tapdleau" $ \tmpdir -> do+ _ <- runGraphvizCommand Dot (digraph' $ toGraph x) Svg (tmpdir ++ "/temp.svg")+ readFile (tmpdir ++ "/temp.svg")+ pdf :: t -> IO FilePath+ pdf x = runGraphvizCommand Dot (digraph' $ toGraph x) Pdf "temp.pdf"++-- | Zipper for trees+class TreeLike z where+ zsingleton :: a -> z a+ move_left :: z a -> z a+ move_right :: z a -> z a+ move_up :: z a-> z a+ move_down :: z a -> z a+ zdelete :: z a -> z a++-- | Pick one element of each list to form new lists.+pickOneOfEach :: [[a]] -> [[a]]+pickOneOfEach [] = [[]]+pickOneOfEach (l:ls) = [ x:xs | x <- l, xs <- pickOneOfEach ls ]++-- | Filter if any element has the propery, otherwise keep all.+filterIfAny :: (a -> Bool) -> [a] -> [a]+filterIfAny f xs = if any f xs then Data.List.filter f xs else xs++-- | Same as @filterIfAny@ but only traversing the list once.+filterIfAny' :: (a -> Bool) -> [a] -> [a]+filterIfAny' f xs = loop xs where+ loop [] = []+ loop [y] = if f y then [y] else xs -- return original list+ loop (y:ys) = if f y then y : Data.List.filter f ys else loop ys++-- | Helper functions for Set & Either+fromEither :: Either a a -> a+fromEither (Left x) = x+fromEither (Right x) = x++leftsSet :: Ord a => Set (Either a a) -> Set a+leftsSet xs = Set.map fromEither $ Set.filter isLeft xs++rightsSet :: Ord a => Set (Either a a) -> Set a+rightsSet xs = Set.map fromEither $ Set.filter isRight xs++leftOfSet :: Ord a => Set (Either a a) -> Set (Either a a)+leftOfSet = Set.filter isLeft++rightOfSet :: Ord a => Set (Either a a) -> Set (Either a a)+rightOfSet = Set.filter isRight++-- | Define another set by providing a filter and a map function.+setComprehension :: (Ord a, Ord b) => (a -> Bool) -> (a -> b) -> Set a -> Set b+setComprehension f g xs = Set.map g (Set.filter f xs)
+ lib/FormM.hs view
@@ -0,0 +1,245 @@+{-# LANGUAGE DeriveGeneric, FlexibleInstances #-}+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}+module FormM where++import qualified Data.Set as Set+import GHC.Generics+import Test.QuickCheck+import Data.List as List+import General+import FormP++-- * The Modal Language++data FormM = BotM | AtM Atom | ConM FormM FormM | DisM FormM FormM | ImpM FormM FormM | Box FormM+ deriving (Eq,Ord,Generic)++instance PropLog FormM where+ neg f = ImpM f BotM+ dis = DisM+ con = ConM+ top = neg BotM+ iff f g = ConM (ImpM f g) (ImpM g f)+ -- Axiom: Γ, p ⇒ ∆, p+ isAtom (AtM _) = True+ isAtom _ = False+ isAxiom _ fs _ = [ ("ax", [])+ | any (\f -> swap f `Set.member` fs) fs ]+ leftBot _ fs _ = [ ("⊥L", []) | Left BotM `Set.member` fs ]+ size BotM = 1+ size (AtM _) = 1+ size (ConM f g) = 1 + size f + size g+ size (DisM f g) = 1 + size f + size g+ size (ImpM f g) = 1 + size f + size g+ size (Box f) = 1 + size f+ subFormulas BotM = [BotM]+ subFormulas (AtM a) = [AtM a]+ subFormulas (ConM f g) = ConM f g : (subFormulas f ++ subFormulas g)+ subFormulas (DisM f g) = DisM f g : (subFormulas f ++ subFormulas g)+ subFormulas (ImpM f g) = ImpM f g : (subFormulas f ++ subFormulas g)+ subFormulas (Box f) = Box f : subFormulas f++dia :: FormM -> FormM+dia f = neg $ Box $ neg f++instance Show FormM where+ show BotM = "⊥"+ show (AtM a) = a+ show (ConM f g) = "(" ++ show f ++ " ∧ " ++ show g ++ ")"+ show (DisM f g) = "(" ++ show f ++ " v " ++ show g ++ ")"+ show (ImpM f g) = "(" ++ show f ++ " → " ++ show g ++ ")"+ show (Box f) = "☐" ++ show f++instance TeX FormM where+ tex BotM = "\\bot"+ tex (AtM ('p':s)) = "p_{" ++ s ++ "}"+ tex (AtM a) = a+ tex (ConM f g) = "(" ++ tex f ++ " \\land " ++ tex g ++ ")"+ tex (DisM f g) = "(" ++ tex f ++ " \\lor " ++ tex g ++ ")"+ tex (ImpM f g) = "(" ++ tex f ++ " \\to " ++ tex g ++ ")"+ tex (Box f) = " \\Box " ++ tex f++instance Arbitrary FormM where+ arbitrary = sized genForm where+ factor = 2+ genForm 0 = oneof [ pure BotM, AtM <$> elements (map return "pqrst")]+ genForm 1 = AtM <$> elements (map return "pqrst")+ genForm n = oneof+ [ pure BotM+ , AtM <$> elements (map return "pqrst")+ , ImpM <$> genForm (n `div` factor) <*> genForm (n `div` factor)+ , ConM <$> genForm (n `div` factor) <*> genForm (n `div` factor)+ , DisM <$> genForm (n `div` factor) <*> genForm (n `div` factor)+ , Box <$> genForm (n `div` factor)+ ]+ shrink = nub . genericShrink++a1,b1,c1,d1,e1 :: FormM+[a1,b1,c1,d1,e1] = map (AtM . return) "12345"++-- * Axioms++-- □(φ → ψ) → (□φ → □ψ) | Holds in all modal logics+kAxiom :: FormM+kAxiom = ImpM (Box (ImpM a1 b1)) (ImpM (Box a1) (Box b1))++-- □φ → □□φ | Holds in D4, K4, K45, D45, S4, GL+fourAxiom :: FormM+fourAxiom = ImpM (Box a1) (Box (Box a1))++-- □φ → φ | Holds in T, S4+tAxiom :: FormM+tAxiom = ImpM (Box a1) a1++-- φ → □♢φ | Holds in B+bAxiom :: FormM+bAxiom = ImpM a1 (Box (dia a1))++-- □(□φ → φ) → □φ | Holds in GL+lobAxiom :: FormM+lobAxiom = ImpM (Box (ImpM (Box a1) a1)) (Box a1)++-- ¬□⊥ | Holds in D, D4, D45, T, S4, S5+consistency :: FormM+consistency = neg . Box $ BotM++-- □□φ → □φ | Holds in T, S4， D45+density :: FormM+density = ImpM (Box (Box a1)) (Box a1)++-- □φ → ♢φ | Holds in D, D4, D45, T, S4 | Also known as seriality+dAxiom :: FormM+dAxiom = ImpM (Box a1) (dia a1)++-- ♢φ → □♢φ | Holds in K45, D45, S5+fiveAxiom :: FormM+fiveAxiom = ImpM (dia a1) (Box (dia a1))++-- Holds in all modal logics+f1 :: FormM+f1 = ImpM (ConM (Box a1) (Box (ImpM a1 b1))) (Box b1)++-- Never holds.+f2 :: FormM+f2 = ImpM (Box (ImpM a1 b1)) (ImpM (Box a1) (ImpM (Box b1) (Box c1)))++-- * For benchmarks+-- □...□φ+boxes :: Int -> FormM -> FormM+boxes 0 f = f+boxes n f = Box (boxes (n-1) f)+-- □...□⊤+boxesTop :: Int -> FormM+boxesTop n = boxes n top+-- □...□⊥+boxesBot :: Int -> FormM+boxesBot n = boxes n BotM+-- □...□φ → □...□□φ | Holds in D4, K4, K45, S4, GL (in logics that have 4)+boxToMoreBox :: Int -> FormM+boxToMoreBox n = ImpM (boxes n a1) (boxes (n + 1) a1)+-- □...□□φ → □...□φ | Holds in T, S4, D45+boxToFewerBox :: Int -> FormM+boxToFewerBox n = ImpM (boxes (n + 1) a1) (boxes n a1)+-- □(□φ → φ) → □...□φ | Holds only in GL+lobBoxes:: Int -> FormM+lobBoxes n = ImpM (Box (ImpM (Box a1) a1)) (boxes n a1)++-- | ◇...◇φ+diamonds :: Int -> FormM -> FormM+diamonds 0 f = f+diamonds n f = Box (boxes (n-1) f)++-- | ◇...◇φ → □...□φ | Holds in D+boxesToDiamonds :: Int -> FormM+boxesToDiamonds n = ImpM (boxes n a1) (diamonds n a1)++-- | Generate a list of n variables+listOfAt :: Int -> [FormM]+listOfAt n = map (AtM . show) $ take n [(3::Integer)..]++-- | Multi-version of the K Axiom+multiVerK :: Int -> FormM+multiVerK n = ImpM (Box (List.foldr ImpM (AtM "1") (listOfAt n)))+ $ foldr (ImpM . Box) (Box (AtM "1")) (listOfAt n)++-- | Similar to multiVerK, but with an extra atom in the premise. Not provable+extraAtK :: Int -> FormM+extraAtK n = ImpM (Box (List.foldr ImpM (AtM "1") (listOfAt n ++ [AtM "2"])))+ $ foldr (ImpM . Box) (Box (AtM "1")) (listOfAt n)++-- | Bench formula for S4. Not provable+negBoxes :: Int -> FormM+negBoxes n = neg $ Box $ neg $ boxes n a1++-- * Embedding Propositional language into Modal language+pTom :: FormP -> FormM+pTom BotP = BotM+pTom (AtP x) = AtM x+pTom (ConP x y) = ConM (pTom x) (pTom y)+pTom (DisP x y) = DisM (pTom x) (pTom y)+pTom (ImpP x y) = ImpM (pTom x) (pTom y)++-- The Gödel–McKinsey–Tarski Translation+translation :: FormP -> FormM+translation BotP = BotM+translation (AtP x) = Box $ AtM x+translation (ConP x y) = ConM (translation x) (translation y)+translation (DisP x y) = DisM (translation x) (translation y)+translation (ImpP x y) = Box $ ImpM (translation x) (translation y)++propFormulasM :: [(String, Int -> FormM)]+propFormulasM = map (fmap (pTom .)) allFormulasP++boxesFormulasM :: [(String, Int -> FormM)]+boxesFormulasM =+ [ ("boxesTop", boxesTop) -- T used to be faster than Z+ , ("boxesBot", boxesBot)+ ]++kFormulasM :: [(String, Int -> FormM)]+kFormulasM =+ [ ("multiVerK", multiVerK) -- T+ , ("boxToMoreBox", boxToMoreBox) -- F+ , ("extraAtK", extraAtK) -- F+ ]++k4FormulasM :: [(String, Int -> FormM)]+k4FormulasM =+ [ ("boxToMoreBox", boxToMoreBox) -- T+ , ("boxToFewerBox", boxToFewerBox) -- F+ ]++glFormulasM :: [(String, Int -> FormM)]+glFormulasM =+ [ ("lobBoxes", lobBoxes) -- T+ , ("boxToFewerBox", boxToFewerBox) -- F+ ]++s4FormulasM :: [(String, Int -> FormM)]+s4FormulasM =+ [ ("negBoxes", negBoxes) -- F+ ]++-- Only go until 20 or you will run out of memory.+hards4FormulasM :: [(String, Int -> FormM)]+hards4FormulasM =+ [ ("boxToFewerBox", boxToFewerBox) -- T+ , ("lobBoxes", lobBoxes) -- F+ ]++-- | Positive modal logic tests+posModalTests :: [(String, FormM)]+posModalTests =+ [ ("k Axiom" , kAxiom)+ , (show f1 , f1)+ , ("boxesTop 10" , boxesTop 10)+ , ("multiVerK 5" , multiVerK 5)+ ]++-- | Negative modal logic tests+negModalTests :: [(String, FormM)]+negModalTests =+ [ (show f2 , f2)+ , ("negBoxes 10" , negBoxes 10)+ , ("boxesBot 10" , boxesBot 10)+ , ("extraAtK 3" , extraAtK 3)]
+ lib/FormM/Parse.y view
@@ -0,0 +1,85 @@+{+{-# OPTIONS_GHC -w #-}+{-# LANGUAGE OverloadedStrings #-}+module FormM.Parse where++import Data.String( IsString(..) )++import General.Token+import General.Lex+import FormM+import General+}++%name parseFormM FormM+%tokentype { Token AlexPosn }+%error { parseError }++%monad { ParseResult } { >>= } { Right }++%token+ TOP { TokenTop _ }+ BOT { TokenBot _ }+ '(' { TokenOB _ }+ ')' { TokenCB _ }+ '&' { TokenCon _ }+ '|' { TokenDis _ }+ '=>' { TokenImpl _ }+ '<->' { TokenEqui _ }+ '~' { TokenNeg _ }+ '<' { TokenDiaL _ }+ '>' { TokenDiaR _ }+ '[' { TokenBoxL _ }+ ']' { TokenBoxR _ }+ '[]' { TokenBox _ }+ '<>' { TokenDia _ }+ STR { TokenString $$ _ }++%right '<->'+%right '=>'+%left '|'+%left '&'+%left '~'++%nonassoc '[' ']' '<' '>' '[]'++%%++FormM : TOP { top }+ | BOT { BotM }+ | '(' FormM ')' { $2 }+ | '~' FormM { neg $2 }+ | FormM '=>' FormM { ImpM $1 $3 }+ | FormM '&' FormM { ConM $1 $3 }+ | FormM '|' FormM { DisM $1 $3 }+ | FormM '<->' FormM { iff $1 $3 }+ | STR { AtM $1 }+ -- TODO multi-modal?+ | '[]' FormM { Box $2 }+ | '[' ']' FormM { Box $3 }+ | '[' STR ']' FormM { Box $4 }+ | '<>' FormM { dia $2 }+ | '<' '>' FormM { dia $3 }+ | '<' STR '>' FormM { dia $4 }++{+type ParseResult a = Either (Int,Int) a++parseError :: [Token AlexPosn] -> ParseResult a+parseError [] = Left (1,1)+parseError (t:ts) = Left (lin,col)+ where (AlexPn _ lin col) = apn t++scanParseSafe :: _ -> String -> ParseResult a+scanParseSafe pfunc input =+ case alexScanTokensSafe input of+ Left pos -> Left pos+ Right lexResult -> case pfunc lexResult of+ Left pos -> Left pos+ Right x -> Right x++instance IsString FormM where+ fromString s = case parseFormM (alexScanTokens s) of+ Left e -> error ("Error at " ++ show e ++ " when parsing " ++ s ++ " \n")+ Right f -> f+}
+ lib/FormP.hs view
@@ -0,0 +1,220 @@+{-# LANGUAGE DeriveGeneric, FlexibleInstances #-}+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}+{-# LANGUAGE InstanceSigs #-}+module FormP where++import Data.List as List+import qualified Data.Set as Set+import GHC.Generics+import Test.QuickCheck+import General++-- | Propositional Formulas+data FormP = BotP | AtP Atom | ConP FormP FormP | DisP FormP FormP | ImpP FormP FormP+ deriving (Eq,Ord,Generic)++instance PropLog FormP where+ neg f = ImpP f BotP+ dis :: FormP -> FormP -> FormP+ dis = DisP+ con = ConP+ top = neg BotP+ iff f g = ConP (ImpP f g) (ImpP g f)+ -- Axiom: Γ, p ⇒ ∆, p+ isAtom (AtP _) = True+ isAtom _ = False+ isAxiom _ fs _ = [ ("ax", [])+ | any (\f -> swap f `Set.member` fs) fs ]+ leftBot _ fs _ = [ ("⊥L", []) | Left BotP `Set.member` fs ]+ size BotP = 1+ size (AtP _) = 1+ size (ConP f g) = 1 + size f + size g+ size (DisP f g) = 1 + size f + size g+ size (ImpP f g) = 1 + size f + size g+ subFormulas BotP = [BotP]+ subFormulas (AtP a) = [AtP a]+ subFormulas (ConP f g) = ConP f g : (subFormulas f ++ subFormulas g)+ subFormulas (DisP f g) = DisP f g : (subFormulas f ++ subFormulas g)+ subFormulas (ImpP f g) = ImpP f g : (subFormulas f ++ subFormulas g)++instance Show FormP where+ show BotP = "⊥"+ show (AtP a) = a+ show (ConP f g) = "(" ++ show f ++ " ∧ " ++ show g ++ ")"+ show (DisP f g) = "(" ++ show f ++ " v " ++ show g ++ ")"+ show (ImpP f g) = "(" ++ show f ++ " → " ++ show g ++ ")"++instance TeX FormP where+ tex BotP = "\\bot"+ tex (AtP ('p':s)) = "p_{" ++ s ++ "}"+ tex (AtP a) = a+ tex (ConP f g) = "(" ++ tex f ++ " \\land " ++ tex g ++ ")"+ tex (DisP f g) = "(" ++ tex f ++ " \\lor " ++ tex g ++ ")"+ tex (ImpP f g) = "(" ++ tex f ++ " \\to " ++ tex g ++ ")"++instance Arbitrary FormP where+ arbitrary = sized genForm where+ factor = 2+ genForm 0 = oneof [ pure BotP, AtP <$> elements (map return "pqrst") ]+ genForm 1 = AtP <$> elements (map return "pqrst")+ genForm n = oneof+ [ pure BotP+ , AtP <$> elements (map return "pqrst")+ , ImpP <$> genForm (n `div` factor) <*> genForm (n `div` factor)+ , ConP <$> genForm (n `div` factor) <*> genForm (n `div` factor)+ , DisP <$> genForm (n `div` factor) <*> genForm (n `div` factor)+ ]+ shrink = nub . genericShrink++o,p,q,r :: FormP+[o,p,q,r] = map (AtP . return) "opqr"++-- | Contradiction+contradiction :: FormP+contradiction = ConP p (neg p)++-- | Excluded middle+excludedMiddle :: FormP+excludedMiddle = DisP p (neg p)++-- | Double negation+doubleNegation :: FormP+doubleNegation = iff (neg (neg p)) p++-- | Right Double negation+doubleNegationR :: FormP+doubleNegationR = ImpP p (neg (neg p))++-- | Peirce's Law+peirce :: FormP+peirce = ImpP (ImpP (ImpP p q) p) p++-- | Double negation of excluded middle+dnEM :: FormP+dnEM = neg $ neg excludedMiddle++-- | List of tests+t1,t2,t3,t4,t5,t6:: FormP+[t1,t2,t3,t4,t5,t6] = [ ImpP p p+ , ImpP (ImpP p (ImpP p q)) (ImpP p q)+ , ImpP (ImpP peirce q) q+ , ConP r excludedMiddle+ , neg $ neg $ ImpP p (ImpP q r)+ , neg $ neg $ DisP p $ neg q+ ]++-- True in IPL+phi :: FormP+phi = ImpP (ConP p (ImpP p q)) (ImpP (ImpP p q) q)++-- * For benchmarks+-- False+conBotR :: Int -> FormP+conBotR k = foldr ConP BotP (replicate k BotP )+-- False+conBotL :: Int -> FormP+conBotL k = foldl ConP BotP (replicate k BotP )+-- False+disBotR :: Int -> FormP+disBotR k = foldr DisP BotP (replicate k BotP )+-- False+disBotL :: Int -> FormP+disBotL k = foldl DisP BotP (replicate k BotP )+-- True+conTopR :: Int -> FormP+conTopR k = foldr ConP top (replicate k top )+-- True+conTopL :: Int -> FormP+conTopL k = foldl ConP top (replicate k top )+-- True+disTopR :: Int -> FormP+disTopR k = foldr DisP top (replicate k top )+-- True+disTopL :: Int -> FormP+disTopL k = foldl DisP top (replicate k top )+-- True in CPL, false in IPL+conPeiR :: Int -> FormP+conPeiR k = foldr ConP peirce (replicate (2*k) peirce )+-- True in CPL, false in IPL+conPeiL :: Int -> FormP+conPeiL k = foldl ConP peirce (replicate (2*k) peirce )+-- True in CPL, false in IPL+disPeiR :: Int -> FormP+disPeiR k = foldr DisP peirce (replicate (2*k) peirce )+-- True in CPL, false in IPL+disPeiL :: Int -> FormP+disPeiL k = foldl DisP peirce (replicate (2*k) peirce )+-- True in CPL, IPL+disPhiPeiR :: Int -> FormP+disPhiPeiR k = foldr DisP phi (replicate (2*k) peirce )+-- True in CPL, IPL+disPhiPeiL :: Int -> FormP+disPhiPeiL k = foldl DisP phi (replicate (2*k) peirce )+-- True in CPL, false in IPL+phiImpPei :: Int -> FormP+phiImpPei 0 = peirce+phiImpPei n = ImpP phi $ phiImpPei (n-1)++allFormulasP :: [(String, Int -> FormP)]+allFormulasP =+ [ ("disPhiPei-R", disPhiPeiR)+ , ("disPhiPei-L", disPhiPeiL)+ , ("disPei-R", disPeiR)+ , ("disPei-L", disPeiL)+ , ("conPei-R", conPeiR)+ , ("conPei-L", conPeiL)+ , ("conBot-R", conBotR)+ , ("conBot-L", conBotL)+ , ("disBot-R", disBotR)+ , ("disBot-L", disBotL)+ , ("conTop-R", conTopR)+ , ("conTop-L", conTopL)+ , ("disTop-R", disTopR)+ , ("disTop-L", disTopL)+ ]++-- | Only go until 20 or you will run out of memory.+hardFormulasP :: [(String, Int -> FormP)]+hardFormulasP =+ [ ("phiImpPei", phiImpPei) ]++-- * Test formulas+-- | Positive classical propositional logic tests+posCPropTests :: [(String, FormP)]+posCPropTests =+ [ ( "Top" , top )+ , ( "Double negation: " ++ show doubleNegation , doubleNegation )+ , ( "Double negation right: " ++ show doubleNegationR , doubleNegationR )+ , ( "Excluded middle: " ++ show excludedMiddle , excludedMiddle )+ , ( "Peirce's law: " ++ show peirce , peirce )+ , ( "Double negation of excluded middle " ++ show dnEM , dnEM )+ , ( show phi , phi )+ , ( show t1 , t1 )+ , ( show t2 , t2 )+ , ( show t3 , t3 )+ , ( "conTopR 10" , conTopR 10 )+ , ( "conTopL 10" , conTopL 10 )+ , ( "disTopR 10" , disTopR 10 )+ , ( "disTopL 10" , disTopL 10 )+ , ( "conPeiR 10" , conPeiR 10 )+ , ( "conPeiL 10" , conPeiL 10 )+ , ( "disPeiR 10" , disPeiR 10 )+ , ( "disPeiL 10" , disPeiL 10 )+ , ( "disPhiPeiR 10" , disPhiPeiR 10 )+ , ( "disPhiPeiL 10" , disPhiPeiL 10 )+ , ( "phiImpPei 10" , phiImpPei 10 )+ ]++-- Negative classical propositional logic tests+negCPropTests :: [(String, FormP)]+negCPropTests =+ [ ( "Bot" , BotP)+ , ( show contradiction , contradiction)+ , ( show t4 , t4)+ , ( show t5 , t5)+ , ( show t6 , t6)+ , ( "conBotR 10" , conBotR 10)+ , ( "conBotL 10" , conBotL 10)+ , ( "disBotR 10" , disBotR 10)+ , ( "disBotL 10" , disBotL 10)+ ]
+ lib/FormP/Parse.y view
@@ -0,0 +1,73 @@+{+{-# OPTIONS_GHC -w #-}+{-# LANGUAGE OverloadedStrings #-}+module FormP.Parse where++import Data.String( IsString(..) )+import Data.Char+import Data.List++import General.Token+import General.Lex+import FormP+import General+}++%name parseFormP FormP+%tokentype { Token AlexPosn }+%error { parseError }++%monad { ParseResult } { >>= } { Right }++%token+ TOP { TokenTop _ }+ BOT { TokenBot _ }+ '(' { TokenOB _ }+ ')' { TokenCB _ }+ '&' { TokenCon _ }+ '|' { TokenDis _ }+ '=>' { TokenImpl _ }+ '<->' { TokenEqui _ }+ '~' { TokenNeg _ }+ STR { TokenString $$ _ }++%right '<->'+%right '=>'+%left '|'+%left '&'+%left '~'++%%++FormP : TOP { top }+ | BOT { BotP }+ | '(' FormP ')' { $2 }+ | '~' FormP { neg $2 }+ | FormP '=>' FormP { ImpP $1 $3 }+ | FormP '&' FormP { ConP $1 $3 }+ | FormP '|' FormP { DisP $1 $3 }+ | FormP '<->' FormP { iff $1 $3 }+ | STR { AtP $1 }++{+type ParseResult a = Either (Int,Int) a++parseError :: [Token AlexPosn] -> ParseResult a+parseError [] = Left (1,1)+parseError (t:ts) = Left (lin,col)+ where (AlexPn _ lin col) = apn t++scanParseSafe :: _ -> String -> ParseResult a+scanParseSafe pfunc input =+ case alexScanTokensSafe input of+ Left pos -> Left pos+ Right lexResult -> case pfunc lexResult of+ Left pos -> Left pos+ Right x -> Right x++instance IsString FormP where+ fromString s = case parseFormP (alexScanTokens s) of+ Left e -> error ("Error at " ++ show e ++ " when parsing " ++ s ++ " \n")+ Right f -> f++}
+ lib/FormP/ParseTPTP.hs view
@@ -0,0 +1,143 @@+module FormP.ParseTPTP where++import Data.Char+import Data.List++import FormP+import FormP.Parse++-- NOTE: This tptp parser was assisted by ChatGPT++-- NOTE by MG: better would be to properly write a TPTP grammar into Parse.y.++rewriteTPTPProblem :: String -> Either (Int,Int) String+rewriteTPTPProblem s = normalizeFormula <$> do+ let blocks = fofBlocks s -- each fof(...) block+ triples = map parseFOFHeader blocks -- [(name,role,formulaText)]+ axTexts = [ f | (_,label,f) <- triples, label == "axiom" ]+ conTexts = [ f | (_,label,f) <- triples, label == "conjecture" ]+ cText <- case conTexts of+ [] -> Left (0,0) -- no conjecture found+ (x:_) -> Right x+ case axTexts of+ [] -> Right cText+ (a:rest) -> Right (foldl (\ fs gs -> fs ++ " & " ++ gs) a rest ++ " -> " ++ cText)++-- NOTE by MG: The function `parseTPTPProblem` does too much, for the executable we+-- only want a `String -> String` before using the existing FormP parser.++-- | Parse .tptp file into a single formula: (A1 & ... & An) -> C+-- where each Ai is a formula with role = axiom, and C is the first conjecture.+parseTPTPProblem :: String -> ParseResult FormP+parseTPTPProblem s = do+ let blocks = fofBlocks s -- each fof(...) block+ triples = map parseFOFHeader blocks -- [(name,role,formulaText)]+ axTexts = [ f | (_,label,f) <- triples, label == "axiom" ]+ conTexts = [ f | (_,label,f) <- triples, label == "conjecture" ]++ cText <- case conTexts of+ [] -> Left (0,0) -- no conjecture found+ (x:_) -> Right x++ -- Parse each formula using the existing FormP parser+ as <- mapM (scanParseSafe parseFormP . normalizeFormula) axTexts+ c <- scanParseSafe parseFormP (normalizeFormula cText)++ case as of+ [] -> Right c+ (a:rest) -> Right (ImpP (foldl ConP a rest) c)++-- | Split the whole file into lines and extract complete fof(...) blocks+-- (each block may span multiple lines).+fofBlocks :: String -> [String]+fofBlocks = go [] [] . lines+ where+ go acc cur [] =+ reverse (if null cur then acc else unlines (reverse cur) : acc)++ go acc cur (l:ls)+ -- Skip comment lines+ | "%" `isPrefixOf` dropWhile isSpace l =+ go acc cur ls++ -- Start of a new fof block: line begins with "fof("+ | "fof(" `isPrefixOf` dropWhile isSpace l =+ let acc' = if null cur+ then acc+ else unlines (reverse cur) : acc+ in go acc' [l] ls++ -- No fof started yet; keep looking+ | null cur =+ go acc cur ls++ -- End of current fof block: line contains "))."+ | "))." `isInfixOf` l =+ go (unlines (reverse (l:cur)) : acc) [] ls++ -- Middle line of the current fof block+ | otherwise =+ go acc (l:cur) ls++-- | Extract (name, role, formulaText) from a fof(...) block.+-- Input is roughly of the form:+-- fof(axiom1,axiom,( ( p1 <=> p2 ) => ( p1 & p2 ) )).+parseFOFHeader :: String -> (String, String, String)+parseFOFHeader block =+ let flat = unwords (words block) -- flatten to a single line, normalize whitespace+ flat' = dropWhile isSpace flat+ -- Drop the leading "fof("+ rest1 = dropPrefix "fof(" flat'+ (name, rest2) = break (== ',') rest1+ rest3 = drop 1 rest2 -- drop first comma+ (rolePart, rest4) = break (== ',') rest3+ role = trim rolePart+ rest5 = drop 1 rest4 -- after second comma we expect "( ... )."+ -- Strip the trailing ")." (fof terminator), keeping the formula's final ')'+ (fmlPart, _) = breakOn ")." rest5+ formulaText = trim fmlPart+ in (trim name, role, formulaText)++-- | Map TPTP boolean constants to the identifiers understood by our lexer (in case they appear).+normalizeFormula :: String -> String+normalizeFormula =+ replace "$false" "false"+ . replace "$true" "true"++-- | Small helper functions+trim :: String -> String+trim = dropWhile isSpace . dropWhileEnd isSpace++dropPrefix :: String -> String -> String+dropPrefix pre s+ | pre `isPrefixOf` s = drop (length pre) s+ | otherwise = s++-- Split the string at the first occurrence of the given substring.+-- Returns (prefix, suffix-without-the-substring).+breakOn :: String -> String -> (String, String)+breakOn pat = go []+ where+ go acc "" = (reverse acc, "")+ go acc s@(c:cs)+ | pat `isPrefixOf` s = (reverse acc, drop (length pat) s)+ | otherwise = go (c:acc) cs++replace :: String -> String -> String -> String+replace old new = go+ where+ go [] = []+ go s@(c:cs)+ | old `isPrefixOf` s = new ++ go (drop (length old) s)+ | otherwise = c : go cs+++-- DEBUGGING++-- Debug helper: print the (name, role, formulaText) triples extracted from a tptp file.+debugTPTP :: String -> IO ()+debugTPTP s = do+ let blocks = fofBlocks s+ triples = map parseFOFHeader blocks+ putStrLn "Blocks/parsing result:"+ mapM_ print triples
+ lib/General.hs view
@@ -0,0 +1,404 @@+{-# LANGUAGE InstanceSigs, FlexibleInstances, LambdaCase #-}++module General where++import Control.Monad+import Data.GraphViz+import Data.GraphViz.Types.Monadic hiding ((-->))+import Data.List as List+import Data.Set (Set)+import qualified Data.Set as Set+import System.IO (hGetContents)+import System.Process+import Basics+import Data.Maybe (fromJust)++type Sequent f = Set (Either f f)++type RuleName = String++-- | A proof as a tree: the Bool flag should start as false and later turn true if provable+data Proof f = Node (Sequent f) (Maybe (RuleName, [Proof f])) Bool+ deriving (Eq,Ord,Show)++-- | Extract truth from a proof+getTruth :: Proof f -> Bool+getTruth (Node _ _ b) = b++-- | Proof size+proofSize :: Proof f -> Int+proofSize (Node _ Nothing _) = 1+proofSize (Node _ (Just (_, ts)) _) = 1 + sum (map proofSize ts)++-- * Histories, Rules, Logics++type History f = [Sequent f]++class HasHistory a where+ histOf :: a f -> History f++class HasProof a where+ proofOf :: a f -> Proof f++-- | A `Rule` takes the history/branch, current sequent and a principal formula.+-- It returns ways to apply a rule, each resulting in possibly multiple branches.+type Rule f = History f -> Sequent f -> Either f f -> [(RuleName, [Sequent f])]++-- | A replace rule only takes a principal formula.+replaceRule :: (Eq f, Ord f) => (Either f f -> [(RuleName, [Sequent f])]) -> Rule f+replaceRule fun _ fs g =+ [ ( fst . head $ fun g+ , [ Set.delete g fs `Set.union` newfs+ | newfs <- snd . head $ fun g ]+ )+ | not (null (fun g)) ]++isApplicable :: History f -> Sequent f -> Either f f -> Rule f -> Bool+isApplicable hs fs f r = not . null $ r hs fs f++isApplicableRule :: History f -> Sequent f -> Rule f -> Bool+isApplicableRule hs fs r = any (\f -> isApplicable hs fs f r) fs++-- | A Logic for a formula type `f`.+data Logic f = Log { name :: String+ , safeRules :: [Rule f]+ , unsafeRules :: [Rule f] }++-- | A prover takes a logic and a formula and returns a Boolean.+type Prover f = Logic f -> f -> Bool++-- * Tree Proofs++newtype ProofWithH f = HP (History f, Proof f)++instance HasHistory ProofWithH where+ histOf (HP (hs, _)) = hs++instance HasProof ProofWithH where+ proofOf (HP (_, pf)) = pf++-- * Zip Proofs++-- | Zipper version of the @Proof@ type.+data ZipProof f = ZP (Proof f) (ZipPath f)+ deriving (Eq,Ord,Show)++data ZipPath f = Top | Step (Sequent f) RuleName (ZipPath f) [Proof f] [Proof f]+ deriving (Eq,Ord,Show)++instance HasHistory ZipPath where+ histOf :: ZipPath f -> History f+ histOf Top = []+ histOf (Step xs _ p _ _) = xs : histOf p++instance HasHistory ZipProof where+ histOf :: ZipProof f -> History f+ histOf (ZP _ zpath) = histOf zpath++instance HasProof ZipProof where+ proofOf (ZP pf _) = pf++-- * Tree-based prover++startForT :: f -> ProofWithH f+startForT f = HP ([], Node (Set.singleton (Right f)) Nothing False)++extendT :: (Eq f, Show f, Ord f) => Logic f -> ProofWithH f -> [ProofWithH f]+extendT l pt@(HP (h, Node fs Nothing _)) =+ case ( List.filter (isApplicableRule h fs) (safeRules l)+ , unsafeRules l ) of+ -- The safe rule r can be applied:+ (r:_ , _ ) ->+ [ HP (h, Node fs (Just (therule, map proofOf ts)) $ all (getTruth . proofOf) ts)+ | (therule, result) <- r h fs f+ , ts <- pickOneOfEach [ extendT l (HP (fs : h, Node newSeqs Nothing False))+ | newSeqs <- result ] ]+ where f = Set.elemAt 0 $ Set.filter (\g -> isApplicable h fs g r) fs+ -- (Using the first possible principal formula.)+ -- At least one unsafe rule can be applied:+ ([], rs@(_:_)) -> List.concatMap applyRule rs+ where+ applyRule r = case List.filter (getTruth . proofOf) nps of+ tp : _ -> [tp]+ [] -> [HP (h, Node fs Nothing False)]+ where+ gs = Set.filter (\g -> isApplicable h fs g r) fs+ nps = concat $ List.concatMap tryExtendT gs+ tryExtendT g = [ List.map (\pwh -> HP (h, Node fs (Just (therule, [proofOf pwh])) $ getTruth (proofOf pwh)))+ $ extendT l (HP (fs : h, Node (head result) Nothing False))+ -- (Using head because we never have branching unsafeRules.)+ | (therule, result) <- r (histOf pt) fs g ]+ -- No rule can be applied, leave proof unfinished:+ ([], [] ) -> [HP (h, Node fs Nothing False)]+extendT _ (HP (_,Node _ (Just _) _)) = error "already extended"++-- | Generate a list of (possibly open) proofs.+proveT :: (Eq f, Show f,Ord f) => Logic f -> f -> [Proof f]+proveT l f = List.map proofOf $ extendT l (startForT f)++-- | Check whether there is a closed proof.+isProvableT :: (Eq f, Show f, Ord f) => Prover f+isProvableT l f = any getTruth (proveT l f)++-- | Generate a list of proofs, only keeping the closed ones if there is any.+proofsT :: (Eq f, Show f,Ord f) => Logic f -> f -> [Proof f]+proofsT l f = filterIfAny' getTruth (proveT l f)++-- | Generate the first closed proof, if there is one+proofT :: (Eq f, Show f,Ord f) => Logic f -> f -> Maybe (Proof f)+proofT l f = case dropWhile (not . getTruth) (proveT l f) of+ [] -> Nothing+ (p : _) -> Just p++provePdfT :: (Ord f,Show f, Eq f) => Logic f -> f -> IO FilePath+provePdfT l f= pdf $ fromJust $ proofT l f++-- * Zipper-based prover++instance TreeLike ZipProof where+ zsingleton x = ZP (Node (Set.singleton (Right x)) Nothing False) Top+ move_left (ZP c (Step s r p xs ys)) =+ if null xs+ then error "cannot go left"+ else ZP (last xs) (Step s r p (init xs) (c:ys))+ move_left _ = error "cannot go left"+ move_right (ZP c (Step s r p xs (y:ys))) = ZP y (Step s r p (xs ++ [c]) ys)+ move_right _ = error "cannot go right"+ move_up (ZP c@(Node _ _ t) (Step s r p xs ys)) =+ let cs = reverse xs ++ [c] ++ ys+ in ZP (Node s (Just (r, cs)) $ t && all getTruth cs) p -- update parent's truth+ move_up _ = error "cannot go up"+ move_down (ZP (Node s (Just (r, x:xs)) _) p) = ZP x (Step s r p [] xs)+ move_down _ = error "cannot go down"+ zdelete (ZP _ (Step s _ Top _ _)) = ZP (Node s Nothing False) Top+ zdelete (ZP _ (Step s _ p _ _)) = ZP (Node s Nothing False) p+ zdelete _ = error "cannot delete top"++-- | Convert a zipper proof to a tree proof by going to the root.+fromZip :: ZipProof f -> Proof f+fromZip (ZP x Top) = x+fromZip zp = fromZip (move_up zp)++-- | Does the node have a right sibling?+hasRsibi :: ZipPath f -> Bool+hasRsibi (Step _ _ _ _ (_:_))= True+hasRsibi _ = False++-- | Does the node have a left sibling?+hasLsibi :: ZipPath f -> Bool+hasLsibi (Step _ _ _ (_:_) _ )= True+hasLsibi _ = False++-- | Switch path, left-biased+-- All the truth manipulations are done by TreeLike method+switch :: ZipProof f -> ZipProof f+switch (ZP pf Top) = ZP pf Top+switch (ZP pf p) = if hasRsibi p+ then move_right (ZP pf p)+ else switch.move_up $ ZP pf p++reverseSwitch :: ZipProof f -> ZipProof f+reverseSwitch (ZP pf Top) = ZP pf Top+reverseSwitch (ZP pf p) = if hasLsibi p+ then move_left (ZP pf p)+ else reverseSwitch.move_up $ ZP pf p++leftAllClosed :: ZipProof f -> Bool+leftAllClosed (ZP _ Top) = True+leftAllClosed zp = getTruth (proofOf zp) && leftAllClosed (reverseSwitch zp)+++startForZ :: f -> ZipProof f+startForZ f = ZP (Node (Set.singleton (Right f)) Nothing False) Top++extendZ :: (Ord f,Eq f) => Logic f -> ZipProof f -> [ZipProof f]+extendZ l zp@(ZP (Node fs Nothing _) p) =+ case ( List.filter (isApplicableRule (histOf zp) fs) (safeRules l)+ , unsafeRules l) of+ -- The safe rule r can be applied:+ (r:_ , _ ) -> let f = Set.elemAt 0 $ Set.filter (\g -> isApplicable (histOf zp) fs g r) fs+ (therule,results) = head $ r (histOf zp) fs f+ newPf = Node fs (Just (therule, [Node newSeq Nothing False | newSeq <- results]))+ -- The truth condition of the parent will always be false, until set true during the switch+ -- If results null, True here of course. We will switch branch+ nextZP+ | null results = switch $ ZP (newPf True) p-- no children, i.e. proved+ | otherwise = move_down $ ZP (newPf False) p -- keep extending the child node+ in extendZ l nextZP+ -- At least one unsafe rule can be applied:+ ([], rs@(_:_)) -> List.concatMap applyRule rs+ where+ applyRule r = case List.filter leftAllClosed nps of+ np : _ -> [np] -- the closed proof+ [] -> [ZP (Node fs Nothing False) p]+ where+ gs = Set.filter (\g -> isApplicable (histOf zp) fs g r) fs+ nps = concat $ List.concatMap tryExtendZ gs+ tryExtendZ g = [ extendZ l (ZP (Node (head result) Nothing False) (Step fs therule p [] []) )+ -- head result as unsaferules won't branch+ | (therule,result) <- r (histOf zp) fs g ]+ -- No rule can be applied, leave proof unfinished:+ ([], [] ) -> [ZP (Node fs Nothing False) p] -- we won't return to top in this case+ -- if provable, will return to top. Not otherwise+extendZ _ zp@(ZP (Node _ (Just _ ) _) _) = [zp] -- needed after switch++-- The easiest way to check whether a zipproof is closed is by always going back to Top and manipulate the truth on the way+-- Then to check the truth of the whole proof, we only need to check the truth condition at the top++-- | Generate a list of (possibly open) zip proofs.+proveZZ :: (Eq f, Ord f) => Logic f -> f -> [ZipProof f]+proveZZ l f = extendZ l (startForZ f)++-- | Generate a list of (possibly open) proofs.+proveZ :: (Eq f, Ord f) => Logic f -> f -> [Proof f]+proveZ l f = List.map fromZip $ proveZZ l f++-- | Check whether there is a closed proof.+isProvableZ :: (Eq f, Ord f) => Prover f+isProvableZ l f = any (getTruth . proofOf) $ List.filter isTop $ proveZZ l f++-- | Generate a list of proofs, only keeping the closed ones if there is any.+proofsZ :: (Eq f, Show f,Ord f) => Logic f -> f -> [Proof f]+proofsZ l f = filterIfAny' getTruth (proveZ l f)++-- | Generate the first closed proof, if there is one+proofZ :: (Eq f, Show f,Ord f) => Logic f -> f -> Maybe (Proof f)+proofZ l f = case dropWhile (not . getTruth) (proveZ l f) of+ [] -> Nothing+ (p : _) -> Just p+++isTop :: ZipProof f -> Bool+isTop (ZP _ Top) = True+isTop _ = False++provePdfZ :: (Ord f,Show f, Eq f) => Logic f -> f -> IO FilePath+provePdfZ l f= pdf $ fromJust $ proofZ l f++-- * Pretty printing, GraphViz and LaTeX output++-- | Pretty print a list of formulas.+ppList :: Show f => [f] -> String+ppList = intercalate " , " . map show++-- | Pretty print a Set of formulas.+ppForm :: Show f => Set f -> String+ppForm ms = ppList (Set.toList ms)++-- | Pretty print a Sequent.+ppSeq :: (Show f, Ord f) => Sequent f -> String+ppSeq xs = ppForm (leftsSet xs) ++ " => " ++ ppForm (rightsSet xs)++-- | Pretty print a proof, with the root last.+ppProof :: (Show f,Ord f) => Proof f -> String+ppProof = ppProof' 0 where+ ppProof' k (Node xs Nothing _) = indent k ++ ppSeq xs+ ppProof' k (Node xs (Just (rule',ts)) _) =+ unlines (map (ppProof' (k + 1)) ts) -- first children+ ++ indent k ++ replicate (length (ppSeq xs)) '-' ++ " (" ++ rule' ++ ")\n" -- then rule+ ++ indent k ++ ppSeq xs -- then current sequent+ indent k = concat (replicate k " ")++-- | Visualisation of proofs.+-- Note that @toGraph@ does not show the Bool flag.+instance (Show f,Ord f) => (DispAble (Proof f)) where+ toGraph = toGraph' "" where+ toGraph' pref (Node fs Nothing _) = do+ node pref [shape PlainText, toLabel $ ppSeq fs]+ node (pref ++ "open") [shape PlainText, toLabel "?"]+ edge pref (pref ++ "open") []+ toGraph' pref (Node fs (Just (rule',ts)) _) = do+ node pref [shape PlainText, toLabel $ ppSeq fs]+ if null ts then do+ node pref [shape PlainText, toLabel $ ppSeq fs]+ node (pref ++ "closed") [shape PlainText, toLabel "."]+ edge pref (pref ++ "closed") [toLabel rule']+ else mapM_ (\(t,y') -> do+ toGraph' (pref ++ show y' ++ ":") t+ edge pref (pref ++ show y' ++ ":") [toLabel rule']+ ) (zip ts [(0::Integer)..])++class TeX a where+ tex :: a -> String+ texFile :: a -> IO ()+ texFile x = do+ let+ pre = unlines [ "\\documentclass[border=2pt]{standalone}"+ , "\\usepackage[utf8]{inputenc}"+ , "\\usepackage{bussproofs,fontenc,graphicx,amssymb,amsmath}"+ , "\\usepackage[pdftex]{hyperref}"+ , "\\hypersetup{pdfborder={0 0 0},breaklinks=true}"+ , "\\begin{document}" ]+ post = "\\DisplayProof\n\\end{document}"+ writeFile "temp.tex" (pre ++ tex x ++ post)+ (_inp, _out, err, pid) <- runInteractiveCommand "pdflatex -interaction=nonstopmode temp.tex"+ _ <- waitForProcess pid+ hGetContents err >>= (\e -> unless (null e) (putStrLn e))++instance (Ord f, TeX f) => TeX (Sequent f) where+ tex xs = texList (Set.toList $ leftsSet xs) ++ " \\Rightarrow " ++ texList (Set.toList $ rightsSet xs)++texList :: TeX f => [f] -> String+texList = intercalate " , " . map (removeOutsideBrackets . tex) where+ removeOutsideBrackets ('(':rest) = init rest+ removeOutsideBrackets s = s++texRuleName :: RuleName -> String+texRuleName r = "$" ++ concatMap f r ++ "$" where+ f = \case+ 'v' -> "\\lor"+ '→' -> "\\to"+ '∧' -> "\\land"+ 'R' -> "{}_{\\mathsf{R}}"+ 'L' -> "{}_{\\mathsf{L}}"+ 'i' -> "^{i}"+ 'T' -> "\\mathsf{T}"+ 'a' -> "\\mathsf{a}"+ 'x' -> "\\mathsf{x}"+ 'c' -> "\\mathsf{c}"+ 'y' -> "\\mathsf{y}"+ 'l' -> "\\mathsf{l}"+ 'e' -> "\\mathsf{e}"+ '⊥' -> "\\bot"+ '4' -> "{}_{\\mathsf{4}}"+ '5' -> "{}_{\\mathsf{5}}"+ 'k' -> "{}_{\\mathsf{k}}"+ '☐' -> "\\Box "+ c -> [c]++-- | Generate LaTeX code to show a proof using the buss package.+-- Does not include @\DisplayProof@ yet.+toBuss :: (Show f, TeX f, Ord f) => Proof f -> String+toBuss (Node fs Nothing _) = "\\AxiomC{ $ " ++ tex fs ++ " $ }"+toBuss (Node fs (Just (rule', ts)) _) =+ concatMap toBuss ts+ +++ case length ts of+ 0 -> "\\AxiomC{\\phantom{I}}\n " ++ r ++ "\\UnaryInfC{ $" ++ tex fs ++ "$ }\n"+ 1 -> r ++ "\\UnaryInfC{ $" ++ tex fs ++ "$ }\n"+ 2 -> r ++ "\\BinaryInfC{ $" ++ tex fs ++ "$ }\n"+ _ -> error "too many premises"+ where r = "\\LeftLabel{" ++ texRuleName rule' ++ "}\n"++instance (Show f, TeX f, Ord f) => TeX (Proof f) where+ tex = toBuss++-- * The Language+type Atom = String++-- | This formula type contains propositional logic.+class PropLog f where+ neg :: f -> f+ con :: f -> f ->f+ dis :: f -> f ->f+ top :: f+ iff :: f -> f -> f+ isAtom :: f -> Bool+ isAxiom :: Rule f+ leftBot :: Rule f+ size :: f -> Int+ subFormulas :: f -> [f]++swap :: Either a b -> Either b a+swap (Left x) = Right x+swap (Right x) = Left x
+ lib/General/Lex.x view
@@ -0,0 +1,71 @@+{+{-# OPTIONS_GHC -w #-}+{-# OPTIONS_GHC -fno-warn-tabs -fno-warn-missing-signatures #-}+module General.Lex where++import General.Token+}++%wrapper "posn"++$dig = 0-9 -- digits+$alf = [a-zA-Z] -- alphabetic characters++tokens :-+ -- ignore whitespace:+ $white+ ;+ -- ignore the word "begin"+ "begin" ;+ -- ignore the word "end"+ "end" ;+ -- keywords and punctuation:+ "(" { \ p _ -> TokenOB p }+ ")" { \ p _ -> TokenCB p }+ -- Formulas:+ "true" { \ p _ -> TokenTop p }+ "⊤" { \ p _ -> TokenTop p }+ "false" { \ p _ -> TokenBot p }+ "⊥" { \ p _ -> TokenBot p }+ "~" { \ p _ -> TokenNeg p }+ "¬" { \ p _ -> TokenNeg p }+ "!" { \ p _ -> TokenNeg p }+ "&" { \ p _ -> TokenCon p }+ "|" { \ p _ -> TokenDis p }+ "v" { \ p _ -> TokenDis p }+ "=>" { \ p _ -> TokenImpl p }+ "→" { \ p _ -> TokenImpl p }+ "->" { \ p _ -> TokenImpl p }+ "-->" { \ p _ -> TokenImpl p }+ "<->" { \ p _ -> TokenEqui p }+ "<=>" { \ p _ -> TokenEqui p }+ "<-->" { \ p _ -> TokenEqui p }+ "↔" { \ p _ -> TokenEqui p }+ "◇" { \ p _ -> TokenDia p }+ "♢" { \ p _ -> TokenDia p }+ "<" { \ p _ -> TokenDiaL p }+ ">" { \ p _ -> TokenDiaR p }+ "☐" { \ p _ -> TokenBox p }+ "◻" { \ p _ -> TokenBox p }+ "□" { \ p _ -> TokenBox p }+ "[]" { \ p _ -> TokenBox p }+ "[" { \ p _ -> TokenBoxL p }+ "]" { \ p _ -> TokenBoxR p }+ -- Strings:+ [$alf $dig _]+ { \ p s -> TokenString s p }+ -- Special chars:+ "𝑝" { \ p _ -> TokenString "p" p }++{+type LexResult a = Either (Int,Int) a++alexScanTokensSafe :: String -> LexResult [Token AlexPosn]+alexScanTokensSafe str = go (alexStartPos,'\n',[],str) where+ go inp@(pos,_,_,str) =+ case (alexScan inp 0) of+ AlexEOF -> Right []+ AlexError ((AlexPn _ line column),_,_,_) -> Left (line,column)+ AlexSkip inp' len -> go inp'+ AlexToken inp' len act -> case (act pos (take len str), go inp') of+ (_, Left lc) -> Left lc+ (x, Right y) -> Right (x : y)+}
+ lib/General/Token.hs view
@@ -0,0 +1,23 @@+module General.Token where++data Token a -- == AlexPn+ = TokenInt {i::Int, apn :: a}+ | TokenString {s::String, apn :: a}+ | TokenTop {apn :: a}+ | TokenBot {apn :: a}+ | TokenPrp {apn :: a}+ | TokenNeg {apn :: a}+ | TokenOB {apn :: a}+ | TokenCB {apn :: a}+ | TokenCon {apn :: a}+ | TokenDis {apn :: a}+ | TokenImpl {apn :: a}+ | TokenEqui {apn :: a}+ | TokenDiaL {apn :: a}+ | TokenDiaR {apn :: a}+ | TokenDia {apn :: a}+ | TokenBoxL {apn :: a}+ | TokenBoxR {apn :: a}+ | TokenBox {apn :: a}++ deriving (Eq,Show)
+ lib/Logic/Modal/D.hs view
@@ -0,0 +1,26 @@+module Logic.Modal.D where++import qualified Data.Set as Set+import General+import Logic.Modal.K+import FormM++d :: Logic FormM+d = Log { name = "D"+ , safeRules = [leftBot, isAxiom, replaceRule safeML]+ , unsafeRules = [boxKrule,boxDrule]+ }++{-+CPL(safe) + ☐k rule(unsafe) + ☐d rule(unsafe):+ Γ ⇒ φ+☐k Γ', □Γ ⇒ □φ, ∆+ Γ, φ ⇒+☐d Γ', □Γ, □φ ⇒ ∆+-}++boxDrule :: Rule FormM+boxDrule _ fs (Left (Box f)) = Set.toList $ Set.map (func f) $ Set.powerSet . removeBoxLeft $ Set.delete (Left (Box f)) fs where+ func :: FormM -> Sequent FormM -> (RuleName,[Sequent FormM])+ func g seqs = ("☐d", [Set.insert (Left g) seqs])+boxDrule _ _ _ = []
+ lib/Logic/Modal/D4.hs view
@@ -0,0 +1,21 @@+module Logic.Modal.D4 where++import General+import Logic.Modal.K+import Logic.Modal.D+import Logic.Modal.K4+import FormM++dfour :: Logic FormM+dfour = Log { name = "D4"+ , safeRules = [leftBot, isAxiom, replaceRule safeML]+ , unsafeRules = [boxDrule,box4rule]+ }++{-+CPL(safe) + ☐d rule(unsafe) + ☐4 rule(unsafe + global loopcheck):+ Γ, φ ⇒+☐d Γ', □Γ, □φ ⇒ ∆+ Γ, □Γ ⇒ φ+☐4 Γ', □Γ ⇒ □φ, ∆+-}
+ lib/Logic/Modal/D45.hs view
@@ -0,0 +1,48 @@+module Logic.Modal.D45 where++import qualified Data.Set as Set+import General+import Logic.Modal.K+import Logic.Modal.K4+import Logic.Modal.K45+import FormM++dfourfive :: Logic FormM+dfourfive = Log { name = "D45"+ , safeRules = [leftBot, isAxiom, replaceRule safeML]+ , unsafeRules = [boxK45rule,boxD45rule]+ }++{-+CPL(safe) + ☐k45 rule(unsafe + global loopcheck) + ☐d45 rule(unsafe + global loopcheck):+ □Γ1, Γ2 ⇒ □∆, φ+☐k45 Γ', □Γ1, □Γ2⇒ □∆, □φ, ∆'+ □Γ1, Γ2 ⇒ □∆+☐d45 Γ', □Γ1, □Γ2⇒ □∆, ∆'+-}++boxD45rule :: Rule FormM+boxD45rule hs fs _ =+ concatMap (globalLoopCheckMap "☐d45" (fs:hs)) premises+ where+ -- { □Γ1 ∪ □Γ2 }+ lBoxes = Set.filter isLeftBox fs+ -- { □Δ }+ rBoxes = Set.filter isRightBox fs+ -- { Δ }+ deltaS :: [Set.Set (Either FormM FormM)]+ deltaS = Set.toList (Set.powerSet rBoxes)+ -- [(□Γ1, □Γ2)]+ boxGammaPartitions :: [(Set.Set (Either FormM FormM), Set.Set (Either FormM FormM))]+ boxGammaPartitions = partitionDrop lBoxes+ -- □Γ1, Γ2 ⇒ □Δ, φ+ premises :: [Set.Set (Either FormM FormM)]+ premises =+ [ Set.unions+ [ boxGamma1+ , Set.map fromBox boxGamma2+ , delta+ ]+ | delta <- deltaS+ , (boxGamma1, boxGamma2) <- boxGammaPartitions+ ]
+ lib/Logic/Modal/GL.hs view
@@ -0,0 +1,30 @@+module Logic.Modal.GL (gl) where++import qualified Data.Set as Set+import Logic.Modal.K+import General+import FormM++gl :: Logic FormM+gl = Log { name = "GL"+ , safeRules = [leftBot, isAxiom, replaceRule safeML, isCycle]+ , unsafeRules = [box4rule]+ }++{-+CPL(safe) + isCycle(safe) + ☐4 rule(unsafe + without loopcheck):+ □Γ, Γ ⇒ φ+☐4 □Γ, Γ' ⇒ ∆, □φ+-}++isCycle :: Rule FormM+isCycle h fs _ = [("cycle", []) | fs `elem` h]++-- | The 4 box rule: without global loopcheck+box4rule :: Rule FormM+box4rule _ fs (Right (Box f)) = concatMap func ss where+ func :: Sequent FormM -> [(RuleName,[Sequent FormM])]+ func seqs = [("☐4", [seqs])]+ ss = Set.map (\s -> Set.unions [Set.singleton (Right f), s, Set.map fromBox s]) ss'+ ss' = Set.powerSet $ Set.filter isLeftBox fs+box4rule _ _ _ = []
+ lib/Logic/Modal/K.hs view
@@ -0,0 +1,45 @@+module Logic.Modal.K where++import qualified Data.Set as Set+import Basics+import General+import FormM++k :: Logic FormM+k = Log { name = "K"+ , safeRules = [leftBot, isAxiom, replaceRule safeML]+ , unsafeRules = [boxKrule]+ }++{-+CPL(safe) + ☐k rule(unsafe):+ Γ ⇒ φ+☐k Γ', □Γ ⇒ □φ, ∆+-}++safeML :: Either FormM FormM -> [(RuleName,[Sequent FormM])]+safeML (Left (ConM f g)) = [("∧L", [Set.fromList [Left f, Left g]])]+safeML (Left (DisM f g)) = [("vL", [Set.singleton (Left f), Set.singleton (Left g)])]+safeML (Left (ImpM f g)) = [("→L", [Set.singleton (Right f), Set.singleton (Left g)])]+safeML (Right (ConM f g)) = [("∧R", [Set.singleton (Right f), Set.singleton (Right g)])]+safeML (Right (DisM f g)) = [("vR", [Set.fromList [Right g, Right f]])]+safeML (Right (ImpM f g)) = [("→R", [Set.fromList [Right g, Left f]])]+safeML _ = []++boxKrule :: Rule FormM+boxKrule _ fs (Right (Box f)) = Set.toList $ Set.map (func f) $ Set.powerSet . removeBoxLeft $ fs where+ func :: FormM -> Sequent FormM -> (RuleName,[Sequent FormM])+ func g seqs = ("☐k", [Set.insert (Right g) seqs])+boxKrule _ _ _ = []++removeBoxLeft :: Sequent FormM -> Sequent FormM+removeBoxLeft = setComprehension isLeftBox fromBox++isLeftBox :: Either FormM FormM -> Bool+isLeftBox (Left (Box _)) = True+isLeftBox _ = False++fromBox :: Either FormM FormM -> Either FormM FormM+fromBox (Left (Box g)) = Left g+fromBox (Right (Box g)) = Right g+fromBox g = g
+ lib/Logic/Modal/K4.hs view
@@ -0,0 +1,29 @@+module Logic.Modal.K4 where++import qualified Data.Set as Set+import General+import Logic.Modal.K+import FormM++kfour :: Logic FormM+kfour = Log { name = "K4"+ , safeRules = [leftBot, isAxiom, replaceRule safeML]+ , unsafeRules = [box4rule]+ }++{-+CPL(safe) + ☐4 rule(unsafe + global loopcheck):+ Γ, □Γ ⇒ φ+☐4 Γ', □Γ ⇒ □φ, ∆+-}++box4rule :: Rule FormM+box4rule hs fs (Right (Box f)) = concatMap (globalLoopCheckMap "☐4" (fs:hs)) ss where+ -- add fs as new seqs could be a subset of fs+ ss = Set.map (\s -> Set.unions [Set.singleton (Right f), s, Set.map fromBox s]) ss'+ ss' = Set.powerSet $ Set.filter isLeftBox fs+box4rule _ _ _ = []++-- Global loopcheck: if not already occur (as a subset) in the history.+globalLoopCheckMap :: RuleName -> History FormM -> Sequent FormM -> [(RuleName,[Sequent FormM])]+globalLoopCheckMap r h seqs = [(r, [seqs]) | not $ any (seqs `Set.isSubsetOf`) h]
+ lib/Logic/Modal/K45.hs view
@@ -0,0 +1,66 @@+module Logic.Modal.K45 where++import qualified Data.Set as Set+import General+import Logic.Modal.K+import Logic.Modal.K4+import FormM++kfourfive :: Logic FormM+kfourfive = Log { name = "K45"+ , safeRules = [leftBot, isAxiom, replaceRule safeML]+ , unsafeRules = [boxK45rule]+ }++{-+CPL(safe) + ☐k45 rule(unsafe + global loopcheck):+ □Γ1, Γ2 ⇒ □∆, φ+☐k45 Γ', □Γ1, □Γ2⇒ □∆, □φ, ∆'+-}++boxK45rule :: Rule FormM+boxK45rule hs fs (Right (Box f)) =+ concatMap (globalLoopCheckMap "☐k45" (fs:hs)) premises+ where+ -- { □Γ1 ∪ □Γ2 }+ lBoxes = Set.filter isLeftBox fs+ -- { □Δ }+ rBoxesRemove = Set.delete (Right (Box f)) (Set.filter isRightBox fs)+ -- all possible □Δ+ deltaS :: [Set.Set (Either FormM FormM)]+ deltaS = Set.toList (Set.powerSet rBoxesRemove)+ -- [(□Γ1, □Γ2)]+ boxGammaPartitions :: [(Set.Set (Either FormM FormM), Set.Set (Either FormM FormM))]+ boxGammaPartitions = partitionDrop lBoxes+ -- □Γ1, Γ2 ⇒ □Δ, φ+ premises :: [Set.Set (Either FormM FormM)]+ premises =+ [ Set.unions+ [ boxGamma1+ , Set.map fromBox boxGamma2+ , delta+ , Set.singleton (Right f)+ ]+ | delta <- deltaS+ , (boxGamma1, boxGamma2) <- boxGammaPartitions+ ]+boxK45rule _ _ _ = []++-- Generate all ordered partitions of a set. O(n·2^n)+partitionDrop :: Ord a => Set.Set a -> [(Set.Set a, Set.Set a)]+partitionDrop s =+ [ (Set.fromDistinctAscList ls, Set.fromDistinctAscList rs)+ | (ls, rs) <- go (Set.toAscList s)+ ]+ where+ -- go produces (leftElemsAsc, rightElemsAsc)+ go [] = [([], [])]+ go (x:xs) =+ let rest = go xs+ in [(l, r) | (l, r) <- rest] -- drop x+ ++ [(l, x:r) | (l, r) <- rest] -- x ∈ Γ1+ ++ [(x:l, r) | (l, r) <- rest] -- x ∈ Γ2++isRightBox :: Either FormM FormM -> Bool+isRightBox (Right (Box _)) = True+isRightBox _ = False
+ lib/Logic/Modal/S4.hs view
@@ -0,0 +1,21 @@+module Logic.Modal.S4 (sfour) where++import General+import Logic.Modal.K+import Logic.Modal.K4+import Logic.Modal.T+import FormM++sfour :: Logic FormM+sfour = Log { name = "S4"+ , safeRules = [leftBot, isAxiom, additionRule safeML, boxTrule]+ , unsafeRules = [box4rule]+ }++{-+saturated CPL(safe + local loopcheck) + ☐t rule(safe + local loopcheck) + ☐4 rule(unsafe + global loopcheck):+ φ, □φ, Γ ⇒ ∆+☐t □φ, Γ ⇒ ∆+ Γ, □Γ ⇒ φ+☐4 Γ', □Γ ⇒ □φ, ∆+-}
+ lib/Logic/Modal/T.hs view
@@ -0,0 +1,40 @@+module Logic.Modal.T where++import qualified Data.Set as Set+import Data.List as List+import General+import Logic.Modal.K+import FormM++t :: Logic FormM+t = Log { name = "T"+ , safeRules = [leftBot, isAxiom, additionRule safeML,boxTrule]+ , unsafeRules = [boxKrule]+ }++{-+saturated CPL(safe + local loopcheck) + ☐t rule(safe +local loopcheck) + ☐k rule(unsafe):+ φ, □φ, Γ ⇒ ∆+☐t □φ, Γ ⇒ ∆+ Γ ⇒ φ+☐k Γ', □Γ ⇒ □φ, ∆+-}++-- | The T box rule. Involve local loopcheck+boxTrule :: Rule FormM+boxTrule _ fs (Left (Box f)) = [("☐t", [Set.insert (Left f) fs]) | Left f `notElem` fs]+boxTrule _ _ _ = []++-- | Local loopcheck: Is this sequent saturated?+localLoopCheck :: Sequent FormM -> Either FormM FormM -> Bool+localLoopCheck fs f = case safeML f of [] -> False+ ((_,results):_) -> not $ any (`Set.isSubsetOf` fs) results++-- Similar as the one in IPL+additionRule :: (Either FormM FormM -> [(RuleName, [Sequent FormM])]) -> Rule FormM+additionRule fun _ fs g =+ [ ( fst . head $ fun g+ , [ fs `Set.union` newfs | newfs <- snd . head $ fun g ] -- not deleting `g` here!+ )+ | localLoopCheck fs g+ , not (List.null (fun g)) ]
+ lib/Logic/Propositional/CPL.hs view
@@ -0,0 +1,35 @@+module Logic.Propositional.CPL (classical) where++import qualified Data.Set as Set+import General+import FormP++classical :: Logic FormP+classical = Log { name = "CPL"+ , safeRules = [leftBot, isAxiom, replaceRule safeCPL]+ , unsafeRules = []+ }++{-+ Γ, φ, ψ ⇒ ∆+∧L Γ, φ ∧ ψ ⇒ ∆+ Γ, φ ⇒ ∆ Γ, ψ ⇒ ∆+∨L Γ, φ ∨ ψ ⇒ ∆+ Γ ⇒ ∆, φ Γ ⇒ ∆, ψ+→L Γ, φ → ψ ⇒ ∆+ Γ ⇒ ∆, φ Γ ⇒ ∆, ψ+∧R Γ ⇒ ∆, φ ∧ ψ+ Γ ⇒ ∆, φ, ψ+∨R Γ ⇒ ∆, φ ∨ ψ+ Γ, φ ⇒ ∆, ψ+→R Γ ⇒ ∆, φ → ψ+-}++safeCPL :: Either FormP FormP -> [(RuleName,[Sequent FormP])]+safeCPL (Left (ConP f g)) = [("∧L", [Set.fromList [Left g, Left f]])]+safeCPL (Left (DisP f g)) = [("vL", [Set.singleton (Left f), Set.singleton (Left g)])]+safeCPL (Left (ImpP f g)) = [("→L", [Set.singleton (Right f), Set.singleton (Left g)])]+safeCPL (Right (ConP f g)) = [("∧R", [Set.singleton (Right f), Set.singleton (Right g)])]+safeCPL (Right (DisP f g)) = [("vR", [Set.fromList [Right g, Right f]])]+safeCPL (Right (ImpP f g)) = [("→R", [Set.fromList [Right g, Left f]])]+safeCPL _ = []
+ lib/Logic/Propositional/IPL.hs view
@@ -0,0 +1,82 @@+module Logic.Propositional.IPL (intui) where++import Data.List as List+import qualified Data.Set as Set+import General+import Basics+import FormP++intui :: Logic FormP+intui = Log { name = "IPL"+ , safeRules = [leftBot, isAxiom, additionRule safeIPL]+ , unsafeRules = [additionRuleNoLoop unsafeIPL]+ }++{-+-- Saturated saferules(local loopcheck)+ Γ, φ ∧ ψ, φ, ψ ⇒ ∆+∧L Γ, φ ∧ ψ ⇒ ∆+ Γ, φ ∨ ψ, φ ⇒ ∆ Γ, φ ∨ ψ, ψ ⇒ ∆+∨L Γ, φ ∨ ψ ⇒ ∆+ Γ, φ → ψ ⇒ ∆, φ Γ, φ → ψ, ψ ⇒ ∆+→iL Γ, φ → ψ ⇒ ∆+ Γ ⇒ ∆, φ ∧ ψ, φ Γ ⇒ ∆, φ ∧ ψ, ψ+∧R Γ ⇒ ∆, φ ∧ ψ+ Γ ⇒ ∆, φ ∨ ψ, φ, ψ+∨R Γ ⇒ ∆, φ ∨ ψ+-- Unsaferule(local + global loopcheck)+ Γ, φ ⇒ ψ+→iR Γ ⇒ ∆, φ → ψ+-}++safeIPL :: Either FormP FormP -> [(RuleName,[Sequent FormP])]+safeIPL (Left (ConP f g)) = [("∧L" , [Set.fromList [Left g, Left f]])]+safeIPL (Left (DisP f g)) = [("vL" , [Set.singleton (Left f), Set.singleton (Left g)])]+safeIPL (Left (ImpP f g)) = [("→iL", [Set.singleton (Right f), Set.singleton (Left g)])]+safeIPL (Right (ConP f g)) = [("∧R" , [Set.singleton (Right f), Set.singleton (Right g)])]+safeIPL (Right (DisP f g)) = [("vR" , [Set.fromList [Right g, Right f]])]+safeIPL _ = []++-- | The R-> rule.+unsafeIPL :: Either FormP FormP -> [(RuleName,[Sequent FormP])]+unsafeIPL (Right (ImpP f g)) = [("→iR", [Set.fromList [Right g, Left f]])]+unsafeIPL _ = []++-- | Local loopcheck: is this sequent saturated?+localLoopCheck :: Sequent FormP -> Either FormP FormP -> Bool+localLoopCheck fs f@(Right (ImpP _ _)) = not $ any (`Set.isSubsetOf` fs) (snd . head . unsafeIPL $ f)+localLoopCheck fs f = case safeIPL f of [] -> False+ ((_,results):_) -> not $ any (`Set.isSubsetOf` fs) results++-- * IPL-specific versions of `replaceRule`.+-- | Like `replaceRule` but keep principal formula (built-in weakening), and block when localLoopCheck.+additionRule :: (Either FormP FormP -> [(RuleName, [Sequent FormP])]) -> Rule FormP+additionRule fun _ fs g =+ [ ( fst . head $ fun g+ , [ fs `Set.union` newfs | newfs <- snd . head $ fun g ] -- not deleting `g` here!+ )+ | localLoopCheck fs g -- local loopcheck+ , not (List.null (fun g)) ]++-- | Helper function for replaceRuleIPLunsafe.+applyIPL :: Sequent FormP -> Either FormP FormP -> [Sequent FormP] -> [Sequent FormP]+applyIPL fs _ = List.map (leftOfSet fs `Set.union`)++-- | Like `additionRule` but also doing a global loopcheck.+additionRuleNoLoop :: (Either FormP FormP -> [(RuleName, [Sequent FormP])]) -> Rule FormP+additionRuleNoLoop fun h fs g =+ [ ( fst . head $ fun g+ , applyIPL fs g $ snd . head . fun $ g+ )+ | localLoopCheck fs g -- local loopcheck+ , globalLoopCheck h fs g -- gobal loopcheck+ , not (List.null (fun g)) ]++-- | Check that the result of applying `unsafeIPL` to `f` does+-- not already occur (as a subset) in the history.+-- Helper function for `replaceRuleIPLunsafe`.+globalLoopCheck :: [Sequent FormP] -> Sequent FormP -> Either FormP FormP -> Bool+globalLoopCheck hs fs f@(Right (ImpP _ _)) =+ let xs = applyIPL fs f (snd (head (unsafeIPL f)))+ in not $ any (Set.isSubsetOf (head xs)) hs+globalLoopCheck _ _ _ = False
+ package.yaml view
@@ -0,0 +1,115 @@+name: GenZ+version: 0.1.0.0+synopsis: Generic Sequent Calculus Prover using the Zipper+description: See README.md for example usage and documentation.+maintainer: Xiaoshuang Yang <thuyxs17@gmail.com>+license: GPL-3+github: XiaoshuangYang999/GenZ+category: Logic++ghc-options: -Wall++extra-source-files:+ - README.md+ - LICENSE+ - stack.yaml+ - package.yaml+ - lib/FormM/Parse.y+ - lib/FormP/Parse.y+ - lib/General/Lex.x+ - exec/index.html++dependencies:+ - array >= 0.5.4 && < 0.6+ - base >= 4.8 && < 5+ - bytestring >= 0.11.5 && < 0.12+ - containers >= 0.6.7 && < 0.7+ - directory >= 1.3.7 && < 1.4+ - filepath >= 1.4.2 && < 1.5+ - graphviz >= 2999.20.2 && < 2999.21+ - hspec >= 2.10.10 && < 2.12+ - multiset >= 0.3.4 && < 0.4+ - process >= 1.6.18 && < 1.7+ - QuickCheck >= 2.4.3 && < 2.19+ - random >= 1.2.1 && < 1.4+ - tagged >= 0.8.7 && < 0.9+ - temporary >= 1.3 && < 1.4++build-tools:+ - alex+ - happy++library:+ source-dirs: lib++executables:+ genz:+ source-dirs: exec+ main: genz.hs+ ghc-options: -Wall -threaded+ dependencies:+ - base >= 4.8 && < 5+ - optparse-applicative >= 0.17.1 && < 0.18+ - GenZ+ genz-web:+ source-dirs: exec+ main: genz-web.hs+ ghc-options: -Wall -threaded+ dependencies:+ - base >= 4.8 && < 5+ - file-embed >= 0.0.15 && < 0.1+ - js-jquery >= 3.3.1 && < 4+ - scotty >= 0.12 && < 0.13+ - GenZ+ - template-haskell >= 2.19.0 && < 2.21+ - text >= 2.0.2 && < 2.1+ - warp >= 3.3.25 && < 3.5++ form-size:+ source-dirs: exec+ main: form-size.hs+ ghc-options: -Wall -threaded+ dependencies:+ - base >= 4.8 && < 5+ - GenZ++ tptp-size:+ source-dirs: exec+ main: tptp-size.hs+ ghc-options: -Wall -threaded+ dependencies:+ - base >= 4.8 && < 5+ - GenZ++tests:+ Test:+ main: Test.hs+ ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N+ source-dirs: test+ dependencies:+ - GenZ+ - QuickCheck >= 2.14.3 && < 2.15+ - hspec++benchmarks:+ runtime:+ source-dirs: bench+ main: runtime.hs+ dependencies:+ - base >= 4.8 && < 5+ - bytestring+ - cassava+ - criterion+ - directory+ - scientific+ - GenZ+ - split+ - vector+ memory:+ source-dirs: bench+ ghc-options: -rtsopts+ main: memory.hs+ dependencies:+ - base >= 4.8 && < 5+ - GenZ+ - weigh
+ stack.yaml view
@@ -0,0 +1,1 @@+resolver: lts-21.25
+ test/Test.hs view
@@ -0,0 +1,379 @@+module Main where++import Test.Hspec+import Test.Hspec.QuickCheck+import Test.QuickCheck+import Data.Bifunctor++import Basics+import General+import FormP+import FormM+import Logic.Propositional.CPL+import Logic.Propositional.IPL+import Logic.Modal.K+import Logic.Modal.K4+import Logic.Modal.GL+import Logic.Modal.S4+import Logic.Modal.T+import Logic.Modal.D+import Logic.Modal.D4+import Logic.Modal.K45+import Logic.Modal.D45++-- | Set a time limit.+-- Test cases will be discarded if they take more than 5 seconds.+limit :: Int+limit = 5 * 1000000 -- in microseconds++-- | Ensure laziness+implies :: Bool -> Bool -> Bool+implies x = if x then id else const True++testsFor :: (Show f, Ord f) => Logic f -> [(String,f)] -> [(String,f)] -> SpecWith ()+testsFor l posExamples negExamples = do+ describe (name l) $ do+ describe "isProvableZ" $ do+ mapM_ (\(s, f) -> it s $ isProvableZ l f) posExamples+ describe "not.isProvableZ" $ do+ mapM_ (\(s, f) -> it s $ not $ isProvableZ l f) negExamples+ describe "isProvableT" $ do+ mapM_ (\(s, f) -> it s $ isProvableT l f) posExamples+ describe "not.isProvableT" $ do+ mapM_ (\(s, f) -> it s $ not $ isProvableT l f) negExamples++conCheck :: (Arbitrary f, Show f, Ord f, PropLog f) => [Logic f] -> SpecWith ()+conCheck = mapM_ $ \l -> do+ prop ("GenZ for " ++ name l) $+ \ f g -> discardAfter limit $ (isProvableZ l f && isProvableZ l g) `implies` isProvableZ l (con f g)+ prop ("GenT for " ++ name l) $+ \ f g -> discardAfter limit $ (isProvableT l f && isProvableT l g) `implies` isProvableT l (con f g)++containTest :: (Arbitrary f, Show f, Ord f, PropLog f) => Logic f -> Logic f -> SpecWith ()+containTest l1 l2 =+ describe ("What is provable in " ++ name l1 ++ " is also provable in " ++ name l2) $ do+ prop "GenZ" $+ \ f -> discardAfter limit $ isProvableZ l1 f `implies` isProvableZ l2 f+ prop "GenT" $+ \ f -> discardAfter limit $ isProvableT l1 f `implies` isProvableT l2 f++agreeTestTranslated :: (Arbitrary f, Show f, Ord f, PropLog f, Arbitrary f', Show f', Ord f', PropLog f') => Logic f -> Logic f' -> (f -> f') -> SpecWith ()+agreeTestTranslated l1 l2 tr = do+ prop "GenZ" $+ \ f -> discardAfter limit $ isProvableZ l1 f === isProvableZ l2 (tr f)+ prop "GenT" $+ \ f -> discardAfter limit $ isProvableT l1 f === isProvableT l2 (tr f)++proverEqTest :: (Arbitrary f, Show f, Ord f, PropLog f) => Logic f -> SpecWith ()+proverEqTest l = do+ prop (name l) $+ \ f -> discardAfter limit $ isProvableZ l f === isProvableT l f++atMostBinTest :: (Arbitrary f, Show f, Ord f, PropLog f) => Logic f -> SpecWith ()+atMostBinTest l = do+ let hasLeqTwoChildren (Node _ Nothing _) = True+ hasLeqTwoChildren (Node _ (Just (_, ts)) _ ) = length ts <= 2 && all hasLeqTwoChildren ts+ prop ("GenZ for " ++ name l) $+ \ f -> discardAfter limit $ all hasLeqTwoChildren $ proveZ l f+ prop ("GenT for " ++ name l) $+ \ f -> discardAfter limit $ all hasLeqTwoChildren $ proveT l f++-- | Check that "isProvable" implies that "proofs" only returns closed proofs.+provabilityTest :: (Arbitrary f, Show f, Ord f, PropLog f) => Logic f -> SpecWith ()+provabilityTest l = do+ prop (name l) $+ \ f -> discardAfter limit $ isProvableZ l f ==> all getTruth (proofsZ l f)+ prop (name l) $+ \ f -> discardAfter limit $ isProvableT l f ==> all getTruth (proofsT l f)++main :: IO ()+main = hspec $ parallel $ do++ describe "Internal helper functions" $ do+ prop "filterIfAny agrees with filterIfAny'" $+ \ f xs -> filterIfAny (applyFun f) (xs :: [Int]) === filterIfAny' (applyFun f) xs+ prop "filterIfAny agrees with filterIfAny' when actually filtering" $+ \ f xs -> filterIfAny (applyFun f) xs /= xs ==>+ filterIfAny (applyFun f) (xs :: [Int]) === filterIfAny' (applyFun f) xs+ modifyMaxDiscardRatio (* 100) $+ prop "filterIfAny agrees with filterIfAny' when changing nothing" $+ \ f xs -> filterIfAny (applyFun f) xs == xs ==>+ filterIfAny (applyFun f) (xs :: [Int]) === filterIfAny' (applyFun f) xs++ describe "Unit tests" $ do+ testsFor classical posCPropTests negCPropTests+ testsFor intui+ [ ( "Top" , top )+ , ( "Double negation right: " ++ show doubleNegationR , doubleNegationR )+ , ( "Double negation of excluded middle " ++ show dnEM , dnEM )+ , ( show phi , phi )+ , ( show t1 , t1 )+ , ( show t2 , t2 )+ , ( show t3 , t3 )+ , ( "conTopR 10" , conTopR 10 )+ , ( "conTopL 10" , conTopL 10 )+ , ( "disTopR 10" , disTopR 10 )+ , ( "disTopL 10" , disTopL 10 )+ , ( "disPhiPeiR 10" , disPhiPeiR 10 )+ , ( "disPhiPeiL 10" , disPhiPeiL 10 )+ ]+ [ ( "Bot" , BotP)+ , ( show contradiction , contradiction)+ , ("Double negation: " ++ show doubleNegation , doubleNegation)+ , ("Excluded middle: " ++ show excludedMiddle , excludedMiddle)+ , ("Peirce's law: " ++ show peirce , peirce)+ , ( show t4 , t4)+ , ( show t5 , t5)+ , ( show t6 , t6)+ , ( "conBotR 10" , conBotR 10)+ , ( "conBotL 10" , conBotL 10)+ , ( "disBotR 10" , disBotR 10)+ , ( "disBotL 10" , disBotL 10)+ , ( "conPeiR 10" , conPeiR 10)+ , ( "conPeiL 10" , conPeiL 10)+ , ( "disPeiR 10" , disPeiR 10)+ , ( "disPeiL 10" , disPeiL 10)+ , ( "phiImpPei 10" , phiImpPei 10)+ ]+ testsFor k+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests)+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ negModalTests+ ++ [ ("4 Axiom" , fourAxiom)+ , ("Lob Axiom" , lobAxiom)+ , ("t Axiom" , tAxiom)+ , ("Consistency" , consistency)+ , ("Density" , density)+ , ("d Axiom" , dAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("B Axiom" , bAxiom)+ , ("lobBoxes 5" , lobBoxes 5)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ , ("boxesToDiamonds 1" , boxToFewerBox 1)+ , ("boxesToDiamonds 5" , boxToFewerBox 5)+ ])+ testsFor kfour+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests+ ++ [ ("4 Axiom" , fourAxiom)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ ])+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ negModalTests+ ++ [ ("Lob Axiom" , lobAxiom)+ , ("t Axiom" , tAxiom)+ , ("Consistency" , consistency)+ , ("Density" , density)+ , ("d Axiom" , dAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("B Axiom" , bAxiom)+ , ("lobBoxes 5" , lobBoxes 5)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ ])+ testsFor t+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests+ ++ [ ("t Axiom" , tAxiom)+ , ("Consistency" , consistency)+ , ("Density" , density)+ , ("d Axiom" , dAxiom)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ ])+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ negModalTests+ ++ [ ("Lob Axiom" , lobAxiom)+ , ("4 Axiom" , fourAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("B Axiom" , bAxiom)+ , ("lobBoxes 5" , lobBoxes 5)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ ])+ testsFor d+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests+ ++ [ ("Consistency" , consistency)+ , ("d Axiom" , dAxiom)+ , ("boxesToDiamonds 1" , boxesToDiamonds 1)+ , ("boxesToDiamonds 5" , boxesToDiamonds 5)+ ])+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ negModalTests+ ++ [ ("Lob Axiom" , lobAxiom)+ , ("t Axiom" , tAxiom)+ , ("4 Axiom" , fourAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("B Axiom" , bAxiom)+ , ("Density" , density)+ , ("lobBoxes 5" , lobBoxes 5)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ ])+ testsFor dfour+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests+ ++ [ ("4 Axiom" , fourAxiom)+ , ("Consistency" , consistency)+ , ("d Axiom" , dAxiom)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ , ("boxesToDiamonds 1" , boxesToDiamonds 1)+ , ("boxesToDiamonds 5" , boxesToDiamonds 5)+ ])+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ negModalTests+ ++ [ ("Lob Axiom" , lobAxiom)+ , ("t Axiom" , tAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("B Axiom" , bAxiom)+ , ("Density" , density)+ , ("lobBoxes 5" , lobBoxes 5)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ ])+ testsFor sfour+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests+ ++ [ ("4 Axiom" , fourAxiom)+ , ("t Axiom" , tAxiom)+ , ("Density" , density)+ , ("Consistency" , consistency)+ , ("dAxiom" , dAxiom)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ ])+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ negModalTests+ ++ [ ("Lob Axiom" , lobAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("B Axiom" , bAxiom)+ , ("lobBoxes 5" , lobBoxes 5)+ ])+ testsFor gl+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests+ ++ [ ("4 Axiom" , fourAxiom)+ , ("Lob Axiom" , lobAxiom)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ , ("lobBoxes 5" , lobBoxes 5)+ ])+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ negModalTests+ ++ [ ("t Axiom" , tAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("Consistency" , consistency)+ , ("Density" , density)+ , ("d Axiom" , dAxiom)+ , ("B Axiom" , bAxiom)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ ])+ testsFor kfourfive+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests+ ++ [ ("4 Axiom" , fourAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ ])+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ negModalTests+ ++ [ ("Lob Axiom" , lobAxiom)+ , ("t Axiom" , tAxiom)+ , ("Consistency" , consistency)+ , ("Density" , density)+ , ("d Axiom" , dAxiom)+ , ("B Axiom" , bAxiom)+ , ("lobBoxes 5" , lobBoxes 5)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ ])+ testsFor dfourfive+ (map (Data.Bifunctor.second pTom) posCPropTests+ ++ posModalTests+ ++ [ ("4 Axiom" , fourAxiom)+ , ("5 Axiom" , fiveAxiom)+ , ("d Axiom" , dAxiom)+ , ("Consistency" , consistency)+ , ("Density" , density)+ , ("boxToMoreBox 5" , boxToMoreBox 5)+ , ("boxToFewerBox 5" , boxToFewerBox 5)+ , ("boxesToDiamonds 1" , boxesToDiamonds 1)+ , ("boxesToDiamonds 5" , boxesToDiamonds 5)+ ])+ (map (Data.Bifunctor.second pTom) negCPropTests+ ++ take 2 negModalTests+ ++ [ ("Lob Axiom" , lobAxiom)+ , ("t Axiom" , tAxiom)+ , ("B Axiom" , bAxiom)+ , ("lobBoxes 5" , lobBoxes 5)+ ])++ describe "Integration tests" $ do+ describe "Equivalence between GenZ and GenT" $ modifyMaxSuccess (const 1000) $ do+ proverEqTest classical+ proverEqTest intui+ proverEqTest k+ proverEqTest kfour+ proverEqTest sfour+ proverEqTest gl+ proverEqTest t+ proverEqTest d+ proverEqTest dfour+ proverEqTest kfourfive+ proverEqTest dfourfive++ describe "Proofs are at most binary" $ do+ atMostBinTest classical+ atMostBinTest intui+ atMostBinTest k+ atMostBinTest kfour+ atMostBinTest sfour+ atMostBinTest gl+ atMostBinTest t+ atMostBinTest d+ atMostBinTest dfour+ atMostBinTest kfourfive+ atMostBinTest dfourfive++ describe "'isProvable' implies that all 'proofs' are closed" $ modifyMaxDiscardRatio (* 10) $ do+ mapM_ provabilityTest [classical,intui]+ mapM_ provabilityTest [k,kfour,sfour,gl,t,d,dfour,kfourfive, dfourfive]++ describe "If f and g isProvable, then Con f g isProvable" $ do+ conCheck [classical,intui]+ conCheck [k,kfour,sfour,gl,t,d,dfour,kfourfive, dfourfive]++ describe "If f isProvable in CPL, then neg neg f isProvable in IPL" $ do+ agreeTestTranslated classical intui (neg . neg)++ describe "Propositional tautologies in modal logics" $ modifyMaxSuccess (const 1000) $ do+ describe "K" $ do+ agreeTestTranslated classical k pTom+ describe "K4" $ do+ agreeTestTranslated classical kfour pTom+ describe "S4" $ do+ agreeTestTranslated classical sfour pTom+ describe "GL" $ do+ agreeTestTranslated classical gl pTom+ describe "T" $ do+ agreeTestTranslated classical t pTom+ describe "D" $ do+ agreeTestTranslated classical d pTom+ describe "D4" $ do+ agreeTestTranslated classical dfour pTom+ describe "K45" $ do+ agreeTestTranslated classical kfourfive pTom+ describe "D45" $ do+ agreeTestTranslated classical dfourfive pTom++ describe "f is provable in IPL iff its translation is provable in S4" $ do+ agreeTestTranslated intui sfour translation++ describe "Modal logics contain tests" $ do+ containTest k kfour+ containTest k d+ containTest d t+ containTest d dfour+ containTest t sfour+ containTest dfour sfour+ containTest kfour gl+ containTest kfour sfour+ containTest kfour kfourfive+ containTest kfourfive dfourfive