diff --git a/GenZ.cabal b/GenZ.cabal new file mode 100644 --- /dev/null +++ b/GenZ.cabal @@ -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 +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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + 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 . + +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 +. + + 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 +. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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 . + +## 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 `&`. | +| `<>`, ``, `◇` | 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: + +![](doc/GL-example.png) + +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 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 +. + +## 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. + + +The original code from the thesis can be found in the `thesis-version` branch. +Ongoing updates and improvements are included in the `main` branch. diff --git a/bench/memory.hs b/bench/memory.hs new file mode 100644 --- /dev/null +++ b/bench/memory.hs @@ -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) + ] diff --git a/bench/runtime.hs b/bench/runtime.hs new file mode 100644 --- /dev/null +++ b/bench/runtime.hs @@ -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) ' ' diff --git a/exec/form-size.hs b/exec/form-size.hs new file mode 100644 --- /dev/null +++ b/exec/form-size.hs @@ -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 diff --git a/exec/genz-web.hs b/exec/genz-web.hs new file mode 100644 --- /dev/null +++ b/exec/genz-web.hs @@ -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 + [ "
INPUT: " ++ textinput ++ "
" + , "
" ++ replicate (col + length ("INPUT:" :: String)) ' ' ++ "^
" + , "
Lexing error in column " ++ show col ++ ".
" ] + 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 + [ "
INPUT: " ++ textinput ++ "
" + , "
" ++ replicate (col + length ("INPUT:" :: String)) ' ' ++ "^
" + , "
Parse error in column " ++ show col ++ ".
" ] + 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 + [ "
Parsed input: " ++ show frm ++ "
" -- TODO pretty? tex? + , if isPrv logic frm + then "PROVED. \n" + else "NOT proved. \n" + , if p_tex /= "" then "
\\( \\begin{prooftree}" ++ p_tex ++ " \\end{prooftree} \\)
" 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." diff --git a/exec/genz.hs b/exec/genz.hs new file mode 100644 --- /dev/null +++ b/exec/genz.hs @@ -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 diff --git a/exec/index.html b/exec/index.html new file mode 100644 --- /dev/null +++ b/exec/index.html @@ -0,0 +1,248 @@ + + + + GenZ prover + + + + + + + + + +

+ This is the web interface of + GenZ. +

+

+ Please choose + + + and a + + +

+

+ Enter a formula below using this syntax or + +

+
+
+| 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                        |
+
+
+
+ + +
running
+
+
+ + + diff --git a/exec/tptp-size.hs b/exec/tptp-size.hs new file mode 100644 --- /dev/null +++ b/exec/tptp-size.hs @@ -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 diff --git a/lib/Basics.hs b/lib/Basics.hs new file mode 100644 --- /dev/null +++ b/lib/Basics.hs @@ -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) diff --git a/lib/FormM.hs b/lib/FormM.hs new file mode 100644 --- /dev/null +++ b/lib/FormM.hs @@ -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)] diff --git a/lib/FormM/Parse.y b/lib/FormM/Parse.y new file mode 100644 --- /dev/null +++ b/lib/FormM/Parse.y @@ -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 +} diff --git a/lib/FormP.hs b/lib/FormP.hs new file mode 100644 --- /dev/null +++ b/lib/FormP.hs @@ -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) + ] diff --git a/lib/FormP/Parse.y b/lib/FormP/Parse.y new file mode 100644 --- /dev/null +++ b/lib/FormP/Parse.y @@ -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 + +} diff --git a/lib/FormP/ParseTPTP.hs b/lib/FormP/ParseTPTP.hs new file mode 100644 --- /dev/null +++ b/lib/FormP/ParseTPTP.hs @@ -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 diff --git a/lib/General.hs b/lib/General.hs new file mode 100644 --- /dev/null +++ b/lib/General.hs @@ -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 diff --git a/lib/General/Lex.x b/lib/General/Lex.x new file mode 100644 --- /dev/null +++ b/lib/General/Lex.x @@ -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) +} diff --git a/lib/General/Token.hs b/lib/General/Token.hs new file mode 100644 --- /dev/null +++ b/lib/General/Token.hs @@ -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) diff --git a/lib/Logic/Modal/D.hs b/lib/Logic/Modal/D.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/D.hs @@ -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 _ _ _ = [] diff --git a/lib/Logic/Modal/D4.hs b/lib/Logic/Modal/D4.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/D4.hs @@ -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 Γ', □Γ ⇒ □φ, ∆ +-} diff --git a/lib/Logic/Modal/D45.hs b/lib/Logic/Modal/D45.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/D45.hs @@ -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 + ] diff --git a/lib/Logic/Modal/GL.hs b/lib/Logic/Modal/GL.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/GL.hs @@ -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 _ _ _ = [] diff --git a/lib/Logic/Modal/K.hs b/lib/Logic/Modal/K.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/K.hs @@ -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 diff --git a/lib/Logic/Modal/K4.hs b/lib/Logic/Modal/K4.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/K4.hs @@ -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] diff --git a/lib/Logic/Modal/K45.hs b/lib/Logic/Modal/K45.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/K45.hs @@ -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 diff --git a/lib/Logic/Modal/S4.hs b/lib/Logic/Modal/S4.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/S4.hs @@ -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 Γ', □Γ ⇒ □φ, ∆ +-} diff --git a/lib/Logic/Modal/T.hs b/lib/Logic/Modal/T.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Modal/T.hs @@ -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)) ] diff --git a/lib/Logic/Propositional/CPL.hs b/lib/Logic/Propositional/CPL.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Propositional/CPL.hs @@ -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 _ = [] diff --git a/lib/Logic/Propositional/IPL.hs b/lib/Logic/Propositional/IPL.hs new file mode 100644 --- /dev/null +++ b/lib/Logic/Propositional/IPL.hs @@ -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 diff --git a/package.yaml b/package.yaml new file mode 100644 --- /dev/null +++ b/package.yaml @@ -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 +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 diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,1 @@ +resolver: lts-21.25 diff --git a/test/Test.hs b/test/Test.hs new file mode 100644 --- /dev/null +++ b/test/Test.hs @@ -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