atp (empty) → 0.1.0.0
raw patch · 25 files changed
+4394/−0 lines, 25 filesdep +Cabaldep +QuickCheckdep +ansi-wl-pprintsetup-changed
Dependencies added: Cabal, QuickCheck, ansi-wl-pprint, atp, base, containers, doctest, generic-random, mtl, process, semigroups, text, tptp
Files
- CHANGELOG.md +5/−0
- LICENSE +674/−0
- Setup.hs +2/−0
- atp.cabal +156/−0
- src/ATP.hs +105/−0
- src/ATP/Codec/TPTP.hs +359/−0
- src/ATP/Error.hs +95/−0
- src/ATP/FOL.hs +29/−0
- src/ATP/FirstOrder/Alpha.hs +100/−0
- src/ATP/FirstOrder/Conversion.hs +100/−0
- src/ATP/FirstOrder/Core.hs +382/−0
- src/ATP/FirstOrder/Derivation.hs +174/−0
- src/ATP/FirstOrder/Occurrence.hs +295/−0
- src/ATP/FirstOrder/Simplification.hs +119/−0
- src/ATP/FirstOrder/Smart.hs +569/−0
- src/ATP/Internal/Enumeration.hs +63/−0
- src/ATP/Pretty/FOL.hs +283/−0
- src/ATP/Prove.hs +119/−0
- src/ATP/Prover.hs +102/−0
- test/Doc/Main.hs +19/−0
- test/Property/Generators.hs +122/−0
- test/Property/Main.hs +319/−0
- test/Property/Modifiers/AlphaEquivalent.hs +65/−0
- test/Property/Modifiers/Simplified.hs +28/−0
- test/Unit/Main.hs +110/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for atp++## 0.1.0.0 -- 2021-01-25++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,674 @@+ GNU GENERAL PUBLIC LICENSE+ Version 3, 29 June 2007++ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++ Preamble++ The GNU General Public License is a free, copyleft license for+software and other kinds of works.++ The licenses for most software and other practical works are designed+to take away your freedom to share and change the works. By contrast,+the GNU General Public License is intended to guarantee your freedom to+share and change all versions of a program--to make sure it remains free+software for all its users. We, the Free Software Foundation, use the+GNU General Public License for most of our software; it applies also to+any other work released this way by its authors. You can apply it to+your programs, too.++ When we speak of free software, we are referring to freedom, not+price. Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+them if you wish), that you receive source code or can get it if you+want it, that you can change the software or use pieces of it in new+free programs, and that you know you can do these things.++ To protect your rights, we need to prevent others from denying you+these rights or asking you to surrender the rights. Therefore, you have+certain responsibilities if you distribute copies of the software, or if+you modify it: responsibilities to respect the freedom of others.++ For example, if you distribute copies of such a program, whether+gratis or for a fee, you must pass on to the recipients the same+freedoms that you received. You must make sure that they, too, receive+or can get the source code. And you must show them these terms so they+know their rights.++ Developers that use the GNU GPL protect your rights with two steps:+(1) assert copyright on the software, and (2) offer you this License+giving you legal permission to copy, distribute and/or modify it.++ For the developers' and authors' protection, the GPL clearly explains+that there is no warranty for this free software. For both users' and+authors' sake, the GPL requires that modified versions be marked as+changed, so that their problems will not be attributed erroneously to+authors of previous versions.++ Some devices are designed to deny users access to install or run+modified versions of the software inside them, although the manufacturer+can do so. This is fundamentally incompatible with the aim of+protecting users' freedom to change the software. The systematic+pattern of such abuse occurs in the area of products for individuals to+use, which is precisely where it is most unacceptable. Therefore, we+have designed this version of the GPL to prohibit the practice for those+products. If such problems arise substantially in other domains, we+stand ready to extend this provision to those domains in future versions+of the GPL, as needed to protect the freedom of users.++ Finally, every program is threatened constantly by software patents.+States should not allow patents to restrict development and use of+software on general-purpose computers, but in those that do, we wish to+avoid the special danger that patents applied to a free program could+make it effectively proprietary. To prevent this, the GPL assures that+patents cannot be used to render the program non-free.++ The precise terms and conditions for copying, distribution and+modification follow.++ TERMS AND CONDITIONS++ 0. Definitions.++ "This License" refers to version 3 of the GNU General Public License.++ "Copyright" also means copyright-like laws that apply to other kinds of+works, such as semiconductor masks.++ "The Program" refers to any copyrightable work licensed under this+License. Each licensee is addressed as "you". "Licensees" and+"recipients" may be individuals or organizations.++ To "modify" a work means to copy from or adapt all or part of the work+in a fashion requiring copyright permission, other than the making of an+exact copy. The resulting work is called a "modified version" of the+earlier work or a work "based on" the earlier work.++ A "covered work" means either the unmodified Program or a work based+on the Program.++ To "propagate" a work means to do anything with it that, without+permission, would make you directly or secondarily liable for+infringement under applicable copyright law, except executing it on a+computer or modifying a private copy. Propagation includes copying,+distribution (with or without modification), making available to the+public, and in some countries other activities as well.++ To "convey" a work means any kind of propagation that enables other+parties to make or receive copies. Mere interaction with a user through+a computer network, with no transfer of a copy, is not conveying.++ An interactive user interface displays "Appropriate Legal Notices"+to the extent that it includes a convenient and prominently visible+feature that (1) displays an appropriate copyright notice, and (2)+tells the user that there is no warranty for the work (except to the+extent that warranties are provided), that licensees may convey the+work under this License, and how to view a copy of this License. If+the interface presents a list of user commands or options, such as a+menu, a prominent item in the list meets this criterion.++ 1. Source Code.++ The "source code" for a work means the preferred form of the work+for making modifications to it. "Object code" means any non-source+form of a work.++ A "Standard Interface" means an interface that either is an official+standard defined by a recognized standards body, or, in the case of+interfaces specified for a particular programming language, one that+is widely used among developers working in that language.++ The "System Libraries" of an executable work include anything, other+than the work as a whole, that (a) is included in the normal form of+packaging a Major Component, but which is not part of that Major+Component, and (b) serves only to enable use of the work with that+Major Component, or to implement a Standard Interface for which an+implementation is available to the public in source code form. A+"Major Component", in this context, means a major essential component+(kernel, window system, and so on) of the specific operating system+(if any) on which the executable work runs, or a compiler used to+produce the work, or an object code interpreter used to run it.++ The "Corresponding Source" for a work in object code form means all+the source code needed to generate, install, and (for an executable+work) run the object code and to modify the work, including scripts to+control those activities. However, it does not include the work's+System Libraries, or general-purpose tools or generally available free+programs which are used unmodified in performing those activities but+which are not part of the work. For example, Corresponding Source+includes interface definition files associated with source files for+the work, and the source code for shared libraries and dynamically+linked subprograms that the work is specifically designed to require,+such as by intimate data communication or control flow between those+subprograms and other parts of the work.++ The Corresponding Source need not include anything that users+can regenerate automatically from other parts of the Corresponding+Source.++ The Corresponding Source for a work in source code form is that+same work.++ 2. Basic Permissions.++ All rights granted under this License are granted for the term of+copyright on the Program, and are irrevocable provided the stated+conditions are met. This License explicitly affirms your unlimited+permission to run the unmodified Program. The output from running a+covered work is covered by this License only if the output, given its+content, constitutes a covered work. This License acknowledges your+rights of fair use or other equivalent, as provided by copyright law.++ You may make, run and propagate covered works that you do not+convey, without conditions so long as your license otherwise remains+in force. You may convey covered works to others for the sole purpose+of having them make modifications exclusively for you, or provide you+with facilities for running those works, provided that you comply with+the terms of this License in conveying all material for which you do+not control copyright. Those thus making or running the covered works+for you must do so exclusively on your behalf, under your direction+and control, on terms that prohibit them from making any copies of+your copyrighted material outside their relationship with you.++ Conveying under any other circumstances is permitted solely under+the conditions stated below. Sublicensing is not allowed; section 10+makes it unnecessary.++ 3. Protecting Users' Legal Rights From Anti-Circumvention Law.++ No covered work shall be deemed part of an effective technological+measure under any applicable law fulfilling obligations under article+11 of the WIPO copyright treaty adopted on 20 December 1996, or+similar laws prohibiting or restricting circumvention of such+measures.++ When you convey a covered work, you waive any legal power to forbid+circumvention of technological measures to the extent such circumvention+is effected by exercising rights under this License with respect to+the covered work, and you disclaim any intention to limit operation or+modification of the work as a means of enforcing, against the work's+users, your or third parties' legal rights to forbid circumvention of+technological measures.++ 4. Conveying Verbatim Copies.++ You may convey verbatim copies of the Program's source code as you+receive it, in any medium, provided that you conspicuously and+appropriately publish on each copy an appropriate copyright notice;+keep intact all notices stating that this License and any+non-permissive terms added in accord with section 7 apply to the code;+keep intact all notices of the absence of any warranty; and give all+recipients a copy of this License along with the Program.++ You may charge any price or no price for each copy that you convey,+and you may offer support or warranty protection for a fee.++ 5. Conveying Modified Source Versions.++ You may convey a work based on the Program, or the modifications to+produce it from the Program, in the form of source code under the+terms of section 4, provided that you also meet all of these conditions:++ a) The work must carry prominent notices stating that you modified+ it, and giving a relevant date.++ b) The work must carry prominent notices stating that it is+ released under this License and any conditions added under section+ 7. This requirement modifies the requirement in section 4 to+ "keep intact all notices".++ c) You must license the entire work, as a whole, under this+ License to anyone who comes into possession of a copy. This+ License will therefore apply, along with any applicable section 7+ additional terms, to the whole of the work, and all its parts,+ regardless of how they are packaged. This License gives no+ permission to license the work in any other way, but it does not+ invalidate such permission if you have separately received it.++ d) If the work has interactive user interfaces, each must display+ Appropriate Legal Notices; however, if the Program has interactive+ interfaces that do not display Appropriate Legal Notices, your+ work need not make them do so.++ A compilation of a covered work with other separate and independent+works, which are not by their nature extensions of the covered work,+and which are not combined with it such as to form a larger program,+in or on a volume of a storage or distribution medium, is called an+"aggregate" if the compilation and its resulting copyright are not+used to limit the access or legal rights of the compilation's users+beyond what the individual works permit. Inclusion of a covered work+in an aggregate does not cause this License to apply to the other+parts of the aggregate.++ 6. Conveying Non-Source Forms.++ You may convey a covered work in object code form under the terms+of sections 4 and 5, provided that you also convey the+machine-readable Corresponding Source under the terms of this License,+in one of these ways:++ a) Convey the object code in, or embodied in, a physical product+ (including a physical distribution medium), accompanied by the+ Corresponding Source fixed on a durable physical medium+ customarily used for software interchange.++ b) Convey the object code in, or embodied in, a physical product+ (including a physical distribution medium), accompanied by a+ written offer, valid for at least three years and valid for as+ long as you offer spare parts or customer support for that product+ model, to give anyone who possesses the object code either (1) a+ copy of the Corresponding Source for all the software in the+ product that is covered by this License, on a durable physical+ medium customarily used for software interchange, for a price no+ more than your reasonable cost of physically performing this+ conveying of source, or (2) access to copy the+ Corresponding Source from a network server at no charge.++ c) Convey individual copies of the object code with a copy of the+ written offer to provide the Corresponding Source. This+ alternative is allowed only occasionally and noncommercially, and+ only if you received the object code with such an offer, in accord+ with subsection 6b.++ d) Convey the object code by offering access from a designated+ place (gratis or for a charge), and offer equivalent access to the+ Corresponding Source in the same way through the same place at no+ further charge. You need not require recipients to copy the+ Corresponding Source along with the object code. If the place to+ copy the object code is a network server, the Corresponding Source+ may be on a different server (operated by you or a third party)+ that supports equivalent copying facilities, provided you maintain+ clear directions next to the object code saying where to find the+ Corresponding Source. Regardless of what server hosts the+ Corresponding Source, you remain obligated to ensure that it is+ available for as long as needed to satisfy these requirements.++ e) Convey the object code using peer-to-peer transmission, provided+ you inform other peers where the object code and Corresponding+ Source of the work are being offered to the general public at no+ charge under subsection 6d.++ A separable portion of the object code, whose source code is excluded+from the Corresponding Source as a System Library, need not be+included in conveying the object code work.++ A "User Product" is either (1) a "consumer product", which means any+tangible personal property which is normally used for personal, family,+or household purposes, or (2) anything designed or sold for incorporation+into a dwelling. In determining whether a product is a consumer product,+doubtful cases shall be resolved in favor of coverage. For a particular+product received by a particular user, "normally used" refers to a+typical or common use of that class of product, regardless of the status+of the particular user or of the way in which the particular user+actually uses, or expects or is expected to use, the product. A product+is a consumer product regardless of whether the product has substantial+commercial, industrial or non-consumer uses, unless such uses represent+the only significant mode of use of the product.++ "Installation Information" for a User Product means any methods,+procedures, authorization keys, or other information required to install+and execute modified versions of a covered work in that User Product from+a modified version of its Corresponding Source. The information must+suffice to ensure that the continued functioning of the modified object+code is in no case prevented or interfered with solely because+modification has been made.++ If you convey an object code work under this section in, or with, or+specifically for use in, a User Product, and the conveying occurs as+part of a transaction in which the right of possession and use of the+User Product is transferred to the recipient in perpetuity or for a+fixed term (regardless of how the transaction is characterized), the+Corresponding Source conveyed under this section must be accompanied+by the Installation Information. But this requirement does not apply+if neither you nor any third party retains the ability to install+modified object code on the User Product (for example, the work has+been installed in ROM).++ The requirement to provide Installation Information does not include a+requirement to continue to provide support service, warranty, or updates+for a work that has been modified or installed by the recipient, or for+the User Product in which it has been modified or installed. Access to a+network may be denied when the modification itself materially and+adversely affects the operation of the network or violates the rules and+protocols for communication across the network.++ Corresponding Source conveyed, and Installation Information provided,+in accord with this section must be in a format that is publicly+documented (and with an implementation available to the public in+source code form), and must require no special password or key for+unpacking, reading or copying.++ 7. Additional Terms.++ "Additional permissions" are terms that supplement the terms of this+License by making exceptions from one or more of its conditions.+Additional permissions that are applicable to the entire Program shall+be treated as though they were included in this License, to the extent+that they are valid under applicable law. If additional permissions+apply only to part of the Program, that part may be used separately+under those permissions, but the entire Program remains governed by+this License without regard to the additional permissions.++ When you convey a copy of a covered work, you may at your option+remove any additional permissions from that copy, or from any part of+it. (Additional permissions may be written to require their own+removal in certain cases when you modify the work.) You may place+additional permissions on material, added by you to a covered work,+for which you have or can give appropriate copyright permission.++ Notwithstanding any other provision of this License, for material you+add to a covered work, you may (if authorized by the copyright holders of+that material) supplement the terms of this License with terms:++ a) Disclaiming warranty or limiting liability differently from the+ terms of sections 15 and 16 of this License; or++ b) Requiring preservation of specified reasonable legal notices or+ author attributions in that material or in the Appropriate Legal+ Notices displayed by works containing it; or++ c) Prohibiting misrepresentation of the origin of that material, or+ requiring that modified versions of such material be marked in+ reasonable ways as different from the original version; or++ d) Limiting the use for publicity purposes of names of licensors or+ authors of the material; or++ e) Declining to grant rights under trademark law for use of some+ trade names, trademarks, or service marks; or++ f) Requiring indemnification of licensors and authors of that+ material by anyone who conveys the material (or modified versions of+ it) with contractual assumptions of liability to the recipient, for+ any liability that these contractual assumptions directly impose on+ those licensors and authors.++ All other non-permissive additional terms are considered "further+restrictions" within the meaning of section 10. If the Program as you+received it, or any part of it, contains a notice stating that it is+governed by this License along with a term that is a further+restriction, you may remove that term. If a license document contains+a further restriction but permits relicensing or conveying under this+License, you may add to a covered work material governed by the terms+of that license document, provided that the further restriction does+not survive such relicensing or conveying.++ If you add terms to a covered work in accord with this section, you+must place, in the relevant source files, a statement of the+additional terms that apply to those files, or a notice indicating+where to find the applicable terms.++ Additional terms, permissive or non-permissive, may be stated in the+form of a separately written license, or stated as exceptions;+the above requirements apply either way.++ 8. Termination.++ You may not propagate or modify a covered work except as expressly+provided under this License. Any attempt otherwise to propagate or+modify it is void, and will automatically terminate your rights under+this License (including any patent licenses granted under the third+paragraph of section 11).++ However, if you cease all violation of this License, then your+license from a particular copyright holder is reinstated (a)+provisionally, unless and until the copyright holder explicitly and+finally terminates your license, and (b) permanently, if the copyright+holder fails to notify you of the violation by some reasonable means+prior to 60 days after the cessation.++ Moreover, your license from a particular copyright holder is+reinstated permanently if the copyright holder notifies you of the+violation by some reasonable means, this is the first time you have+received notice of violation of this License (for any work) from that+copyright holder, and you cure the violation prior to 30 days after+your receipt of the notice.++ Termination of your rights under this section does not terminate the+licenses of parties who have received copies or rights from you under+this License. If your rights have been terminated and not permanently+reinstated, you do not qualify to receive new licenses for the same+material under section 10.++ 9. Acceptance Not Required for Having Copies.++ You are not required to accept this License in order to receive or+run a copy of the Program. Ancillary propagation of a covered work+occurring solely as a consequence of using peer-to-peer transmission+to receive a copy likewise does not require acceptance. However,+nothing other than this License grants you permission to propagate or+modify any covered work. These actions infringe copyright if you do+not accept this License. Therefore, by modifying or propagating a+covered work, you indicate your acceptance of this License to do so.++ 10. Automatic Licensing of Downstream Recipients.++ Each time you convey a covered work, the recipient automatically+receives a license from the original licensors, to run, modify and+propagate that work, subject to this License. You are not responsible+for enforcing compliance by third parties with this License.++ An "entity transaction" is a transaction transferring control of an+organization, or substantially all assets of one, or subdividing an+organization, or merging organizations. If propagation of a covered+work results from an entity transaction, each party to that+transaction who receives a copy of the work also receives whatever+licenses to the work the party's predecessor in interest had or could+give under the previous paragraph, plus a right to possession of the+Corresponding Source of the work from the predecessor in interest, if+the predecessor has it or can get it with reasonable efforts.++ You may not impose any further restrictions on the exercise of the+rights granted or affirmed under this License. For example, you may+not impose a license fee, royalty, or other charge for exercise of+rights granted under this License, and you may not initiate litigation+(including a cross-claim or counterclaim in a lawsuit) alleging that+any patent claim is infringed by making, using, selling, offering for+sale, or importing the Program or any portion of it.++ 11. Patents.++ A "contributor" is a copyright holder who authorizes use under this+License of the Program or a work on which the Program is based. The+work thus licensed is called the contributor's "contributor version".++ A contributor's "essential patent claims" are all patent claims+owned or controlled by the contributor, whether already acquired or+hereafter acquired, that would be infringed by some manner, permitted+by this License, of making, using, or selling its contributor version,+but do not include claims that would be infringed only as a+consequence of further modification of the contributor version. For+purposes of this definition, "control" includes the right to grant+patent sublicenses in a manner consistent with the requirements of+this License.++ Each contributor grants you a non-exclusive, worldwide, royalty-free+patent license under the contributor's essential patent claims, to+make, use, sell, offer for sale, import and otherwise run, modify and+propagate the contents of its contributor version.++ In the following three paragraphs, a "patent license" is any express+agreement or commitment, however denominated, not to enforce a patent+(such as an express permission to practice a patent or covenant not to+sue for patent infringement). To "grant" such a patent license to a+party means to make such an agreement or commitment not to enforce a+patent against the party.++ If you convey a covered work, knowingly relying on a patent license,+and the Corresponding Source of the work is not available for anyone+to copy, free of charge and under the terms of this License, through a+publicly available network server or other readily accessible means,+then you must either (1) cause the Corresponding Source to be so+available, or (2) arrange to deprive yourself of the benefit of the+patent license for this particular work, or (3) arrange, in a manner+consistent with the requirements of this License, to extend the patent+license to downstream recipients. "Knowingly relying" means you have+actual knowledge that, but for the patent license, your conveying the+covered work in a country, or your recipient's use of the covered work+in a country, would infringe one or more identifiable patents in that+country that you have reason to believe are valid.++ If, pursuant to or in connection with a single transaction or+arrangement, you convey, or propagate by procuring conveyance of, a+covered work, and grant a patent license to some of the parties+receiving the covered work authorizing them to use, propagate, modify+or convey a specific copy of the covered work, then the patent license+you grant is automatically extended to all recipients of the covered+work and works based on it.++ A patent license is "discriminatory" if it does not include within+the scope of its coverage, prohibits the exercise of, or is+conditioned on the non-exercise of one or more of the rights that are+specifically granted under this License. You may not convey a covered+work if you are a party to an arrangement with a third party that is+in the business of distributing software, under which you make payment+to the third party based on the extent of your activity of conveying+the work, and under which the third party grants, to any of the+parties who would receive the covered work from you, a discriminatory+patent license (a) in connection with copies of the covered work+conveyed by you (or copies made from those copies), or (b) primarily+for and in connection with specific products or compilations that+contain the covered work, unless you entered into that arrangement,+or that patent license was granted, prior to 28 March 2007.++ Nothing in this License shall be construed as excluding or limiting+any implied license or other defenses to infringement that may+otherwise be available to you under applicable patent law.++ 12. No Surrender of Others' Freedom.++ If conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License. If you cannot convey a+covered work so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you may+not convey it at all. For example, if you agree to terms that obligate you+to collect a royalty for further conveying from those to whom you convey+the Program, the only way you could satisfy both those terms and this+License would be to refrain entirely from conveying the Program.++ 13. Use with the GNU Affero General Public License.++ Notwithstanding any other provision of this License, you have+permission to link or combine any covered work with a work licensed+under version 3 of the GNU Affero General Public License into a single+combined work, and to convey the resulting work. The terms of this+License will continue to apply to the part which is the covered work,+but the special requirements of the GNU Affero General Public License,+section 13, concerning interaction through a network will apply to the+combination as such.++ 14. Revised Versions of this License.++ The Free Software Foundation may publish revised and/or new versions of+the GNU General Public License from time to time. Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++ Each version is given a distinguishing version number. If the+Program specifies that a certain numbered version of the GNU General+Public License "or any later version" applies to it, you have the+option of following the terms and conditions either of that numbered+version or of any later version published by the Free Software+Foundation. If the Program does not specify a version number of the+GNU General Public License, you may choose any version ever published+by the Free Software Foundation.++ If the Program specifies that a proxy can decide which future+versions of the GNU General Public License can be used, that proxy's+public statement of acceptance of a version permanently authorizes you+to choose that version for the Program.++ Later license versions may give you additional or different+permissions. However, no additional obligations are imposed on any+author or copyright holder as a result of your choosing to follow a+later version.++ 15. Disclaimer of Warranty.++ THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY+APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM+IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.++ 16. Limitation of Liability.++ IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF+SUCH DAMAGES.++ 17. Interpretation of Sections 15 and 16.++ If the disclaimer of warranty and limitation of liability provided+above cannot be given local legal effect according to their terms,+reviewing courts shall apply local law that most closely approximates+an absolute waiver of all civil liability in connection with the+Program, unless a warranty or assumption of liability accompanies a+copy of the Program in return for a fee.++ END OF TERMS AND CONDITIONS++ How to Apply These Terms to Your New Programs++ If you develop a new program, and you want it to be of the greatest+possible use to the public, the best way to achieve this is to make it+free software which everyone can redistribute and change under these terms.++ To do so, attach the following notices to the program. It is safest+to attach them to the start of each source file to most effectively+state the exclusion of warranty; and each file should have at least+the "copyright" line and a pointer to where the full notice is found.++ <one line to give the program's name and a brief idea of what it does.>+ Copyright (C) <year> <name of author>++ This program is free software: you can redistribute it and/or modify+ it under the terms of the GNU General Public License as published by+ the Free Software Foundation, either version 3 of the License, or+ (at your option) any later version.++ This program is distributed in the hope that it will be useful,+ but WITHOUT ANY WARRANTY; without even the implied warranty of+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the+ GNU General Public License for more details.++ You should have received a copy of the GNU General Public License+ along with this program. If not, see <http://www.gnu.org/licenses/>.++Also add information on how to contact you by electronic and paper mail.++ If the program does terminal interaction, make it output a short+notice like this when it starts in an interactive mode:++ <program> Copyright (C) <year> <name of author>+ This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'.+ This is free software, and you are welcome to redistribute it+ under certain conditions; type `show c' for details.++The hypothetical commands `show w' and `show c' should show the appropriate+parts of the General Public License. Of course, your program's commands+might be different; for a GUI interface, you would use an "about box".++ You should also get your employer (if you work as a programmer) or school,+if any, to sign a "copyright disclaimer" for the program, if necessary.+For more information on this, and how to apply and follow the GNU GPL, see+<http://www.gnu.org/licenses/>.++ The GNU General Public License does not permit incorporating your program+into proprietary programs. If your program is a subroutine library, you+may consider it more useful to permit linking proprietary applications with+the library. If this is what you want to do, use the GNU Lesser General+Public License instead of this License. But first, please read+<http://www.gnu.org/philosophy/why-not-lgpl.html>.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ atp.cabal view
@@ -0,0 +1,156 @@+cabal-version: 2.4+name: atp+version: 0.1.0.0+synopsis: Interface to automated theorem provers+description:+ Express theorems in first-order logic and automatically prove them using+ third-party reasoning tools.+homepage: https://github.com/aztek/atp+bug-reports: https://github.com/aztek/atp/issues+license: GPL-3.0-only+license-file: LICENSE+author: Evgenii Kotelnikov+maintainer: evgeny.kotelnikov@gmail.com+category: Theorem Provers, Formal Methods, Logic, Math+tested-with:+ GHC == 7.10.3,+ GHC == 8.0.2,+ GHC == 8.2.2,+ GHC == 8.4.4,+ GHC == 8.6.5,+ GHC == 8.8.4,+ GHC == 8.10.3++extra-source-files:+ CHANGELOG.md+ test/**/*.hs++source-repository head+ type: git+ location: git://github.com/aztek/atp.git++flag Werror+ default: False+ manual: True++-- Build test suites that require some theorem provers to be installed.+flag provers+ default: False+ manual: True++library+ hs-source-dirs: src+ default-language: Haskell2010+ exposed-modules:+ ATP+ ATP.Codec.TPTP+ ATP.Error+ ATP.FOL+ ATP.Pretty.FOL+ ATP.Prove+ ATP.Prover+ other-modules:+ ATP.Internal.Enumeration+ ATP.FirstOrder.Core+ ATP.FirstOrder.Alpha+ ATP.FirstOrder.Smart+ ATP.FirstOrder.Simplification+ ATP.FirstOrder.Occurrence+ ATP.FirstOrder.Conversion+ ATP.FirstOrder.Derivation+ ghc-options:+ -Wall+ if flag(Werror)+ ghc-options: -Werror+ build-depends:+ base >= 4.8 && < 5.0,+ text >= 1.2.3 && < 1.3,+ tptp >= 0.1.3 && < 0.2,+ containers >= 0.5.11 && < 0.7,+ mtl >= 2.2 && < 3.0,+ ansi-wl-pprint >= 0.6.6 && < 0.7,+ process >= 1.6.3 && < 1.7+ if impl(ghc < 8)+ ghc-options:+ -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns+ build-depends:+ semigroups >= 0.18 && < 1.0+ if impl(ghc >= 8)+ ghc-options:+ -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns+ -Wredundant-constraints++test-suite property+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ default-language: Haskell2010+ main-is: Property/Main.hs+ other-modules:+ Property.Generators+ Property.Modifiers.AlphaEquivalent+ Property.Modifiers.Simplified+ ghc-options:+ -Wall -threaded+ if flag(Werror)+ ghc-options: -Werror+ build-depends:+ base,+ containers,+ text,+ mtl,+ generic-random >= 1.2.0.0 && < 1.3,+ QuickCheck >= 2.4 && < 3.0,+ atp+ if impl(ghc < 8)+ ghc-options:+ -fwarn-incomplete-record-updates -fwarn-incomplete-uni-patterns+ build-depends:+ semigroups >= 0.18 && < 1.0+ if impl(ghc >= 8)+ ghc-options:+ -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns+ -Wredundant-constraints++test-suite doc+ type: exitcode-stdio-1.0+ hs-source-dirs: test+ default-language: Haskell2010+ main-is: Doc/Main.hs+ other-modules:+ Property.Generators+ ghc-options:+ -Wall -threaded+ if flag(Werror)+ ghc-options: -Werror+ -- TODO: Make it work+ buildable: False+ build-depends:+ base,+ containers,+ text,+ generic-random >= 1.2.0.0 && < 1.3,+ QuickCheck >= 2.4 && < 3.0,+ atp,+ doctest++test-suite unit+ type: detailed-0.9+ hs-source-dirs: test+ default-language: Haskell2010+ test-module: Unit.Main+ ghc-options:+ -Wall -threaded+ if flag(Werror)+ ghc-options: -Werror+ if flag(provers)+ buildable: True+ else+ buildable: False+ -- TODO: Workaround the pesky bug in ghc 8.0+ -- https://stackoverflow.com/q/39310043/1344648+ if (impl(ghc >= 8.0.0)) && (impl(ghc < 8.1.0))+ buildable: False+ build-depends:+ base,+ Cabal >= 1.16.0,+ atp
+ src/ATP.hs view
@@ -0,0 +1,105 @@+{-|+Module : ATP+Description : Interface to automated theorem provers.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental++Express theorems in first-order logic and automatically prove them+using third-party reasoning tools.+-}++module ATP (+ -- * First-order logic+ -- $fol+ module ATP.FOL,++ -- * Pretty printing for formulas, theorems and proofs+ -- $pretty+ module ATP.Pretty.FOL,++ -- * Interface to automated theorem provers+ -- $prove+ module ATP.Prove,++ -- * Models of automated theorem provers+ -- $prover+ module ATP.Prover,++ -- * Error handling+ -- $error+ module ATP.Error+) where++import ATP.FOL+import ATP.Pretty.FOL+import ATP.Prove+import ATP.Prover+import ATP.Error++-- $fol+-- Consider the following classical logical syllogism.+--+-- /All humans are mortal. Socrates is a human. Therefore, Socrates is mortal./+--+-- We can formalize it in first-order logic as follows.+--+-- > human, mortal :: UnaryPredicate+-- > human = UnaryPredicate "human"+-- > mortal = UnaryPredicate "mortal"+-- >+-- > socrates :: Constant+-- > socrates = "socrates"+-- >+-- > humansAreMortal, socratesIsHuman, socratesIsMortal :: Formula+-- > humansAreMortal = forall $ \x -> human x ==> mortal x+-- > socratesIsHuman = human socrates+-- > socratesIsMortal = mortal socrates+-- >+-- > syllogism :: Theorem+-- > syllogism = [humansAreMortal, socratesIsHuman] |- socratesIsMortal++-- $pretty+-- 'pprint' pretty-prints theorems and proofs.+--+-- >>> pprint syllogism+-- Axiom 1. ∀ x . (human(x) => mortal(x))+-- Axiom 2. human(socrates)+-- Conjecture. mortal(socrates)++-- $prove+-- 'prove' runs a 'defaultProver' and parses the proof that it produces.+--+-- >>> prove syllogism >>= pprint+-- Found a proof by refutation.+-- 1. human(socrates) [axiom]+-- 2. ∀ x . (human(x) => mortal(x)) [axiom]+-- 3. mortal(socrates) [conjecture]+-- 4. ￢mortal(socrates) [negated conjecture 3]+-- 5. ∀ x . (￢human(x) ⋁ mortal(x)) [variable_rename 2]+-- 6. mortal(x) ⋁ ￢human(x) [split_conjunct 5]+-- 7. mortal(socrates) [paramodulation 6, 1]+-- 8. ⟘ [cn 4, 7]+--+-- The proof returned by the theorem prover is a directed acyclic graph of+-- logical inferences. Each logical 'Inference' is a step of the proof that+-- derives a conclusion from a set of premises using an inference 'Rule'.+-- The proof starts with negating the conjecture and ends with a 'Contradiction'+-- and therefore is a proof by 'Refutation'.+--+-- Theorem provers implement elaborate proof search strategies that can be+-- tweaked in many different ways. 'ProvingOptions' contain values of the input+-- parameters to theorem provers. 'prove' uses 'defaultOptions' and 'proveWith'+-- run a specified set of options.++-- $prover+-- By default 'prove' runs the E theorem prover ('eprover'). Currently,+-- 'eprover' and 'vampire' are supported.+--+-- 'proveUsing' runs a specified theorem prover.++-- $error+-- A theorem prover might not succeed to construct a proof. Therefore the result+-- of 'prove' is wrapped in the 'Partial' monad that represents a possible+-- 'Error', for example 'TimeLimitError' or 'ParsingError'.
+ src/ATP/Codec/TPTP.hs view
@@ -0,0 +1,359 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiWayIf #-}+{-# LANGUAGE OverloadedStrings #-}++{-|+Module : ATP.Codec.TPTP+Description : Coding and decoding of unsorted first-order logic in TPTP.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module ATP.Codec.TPTP (+ encode,+ decode,+ encodeFormula,+ decodeFormula,+ encodeClause,+ decodeClause,+ encodeTheorem,+ encodeClauses,+ decodeSolution+) where++import Control.Applicative (liftA2)+import Control.Monad (foldM)+import Control.Monad.Trans (lift)+import Data.Functor (($>))+import Data.List (genericIndex, find)+import qualified Data.List.NonEmpty as NE (toList)+import Data.Map (Map, (!))+#if !MIN_VERSION_base(4, 11, 0)+import Data.Semigroup (Semigroup(..))+#endif+import Data.Text (Text)+import qualified Data.Text as T+import qualified Data.TPTP as TPTP++import ATP.Internal.Enumeration+import ATP.Error+import ATP.FOL+++-- * Coding and decoding++-- | Encode a variable in TPTP.+--+-- >>> encodeVar 0+-- Var "X"+--+-- >>> encodeVar 1+-- Var "Y"+--+-- >>> encodeVar 7+-- Var "X1"+--+-- >>> encodeVar (-1)+-- Var "YY"+--+-- >>> encodeVar (-7)+-- Var "XX1"+--+-- @encodeVar@ is injective.+--+-- prop> (v == v') == (encodeVar v == encodeVar v')+--+encodeVar :: Var -> TPTP.Var+encodeVar v = TPTP.Var $ genericIndex variables (abs v)+ where+ variables :: [Text]+ variables = liftA2 prime [0..] ["X", "Y", "Z", "P", "Q", "R", "T"]++ prime :: Integer -> Text -> Text+ prime n w = letter <> index+ where+ letter = if v >= 0 then w else w <> w+ index = if n == 0 then T.empty else T.pack (show n)++type Substitutions = EnumerationT TPTP.Var Partial++-- | Encode a function symbol in TPTP.+encodeFunction :: FunctionSymbol -> TPTP.Name TPTP.Function+encodeFunction (FunctionSymbol s) = TPTP.Defined (TPTP.Atom s)++-- | Decode a function symbol from TPTP.+decodeFunction :: TPTP.Name s -> Partial FunctionSymbol+decodeFunction = \case+ TPTP.Defined (TPTP.Atom s) -> return (FunctionSymbol s)+ TPTP.Reserved{} -> parsingError "reserved functions are not supported"++-- | Encode a predicate symbol in TPTP.+encodePredicate :: PredicateSymbol -> TPTP.Name TPTP.Predicate+encodePredicate (PredicateSymbol p) = TPTP.Defined (TPTP.Atom p)++-- | Encode a term in TPTP.+encodeTerm :: Term -> TPTP.Term+encodeTerm = \case+ Variable v -> TPTP.Variable (encodeVar v)+ Function f ts -> TPTP.Function (encodeFunction f) (fmap encodeTerm ts)++-- | Decode a term from TPTP.+decodeTermS :: TPTP.Term -> Substitutions Term+decodeTermS = \case+ TPTP.Function f ts -> Function <$> lift (decodeFunction f) <*> traverse decodeTermS ts+ TPTP.Variable v -> Variable <$> enumerate v+ TPTP.Number{} -> lift $ parsingError "numbers are not supported"+ TPTP.DistinctTerm{} -> lift $ parsingError "distinct objects are not supported"++-- | Encode a literal in TPTP.+encodeLiteral :: Literal -> TPTP.Literal+encodeLiteral = \case+ Predicate p ts -> TPTP.Predicate (encodePredicate p) (fmap encodeTerm ts)+ Equality a b -> TPTP.Equality (encodeTerm a) TPTP.Positive (encodeTerm b)+ Propositional b -> TPTP.Predicate (TPTP.Reserved (TPTP.Standard p)) []+ where p = if b then TPTP.Tautology else TPTP.Falsum++-- | Decode a literal from TPTP.+decodeLiteral :: TPTP.Literal -> Substitutions (Signed Literal)+decodeLiteral = \case+ TPTP.Predicate p ts -> do+ p' <- lift (decodePredicate p)+ ts' <- traverse decodeTermS ts+ return $ Signed Positive (p' ts')+ TPTP.Equality a s b -> decodeEquality s <$> decodeTermS a <*> decodeTermS b++decodePredicate :: TPTP.Name TPTP.Predicate -> Partial ([Term] -> Literal)+decodePredicate = \case+ TPTP.Defined (TPTP.Atom p) -> return $ Predicate (PredicateSymbol p)+ TPTP.Reserved (TPTP.Standard TPTP.Tautology) -> return $ const (Propositional True)+ TPTP.Reserved (TPTP.Standard TPTP.Falsum) -> return $ const (Propositional False)+ TPTP.Reserved (TPTP.Standard p) ->+ parsingError $ "unsupported standard reserved predicate " <> show p+ TPTP.Reserved TPTP.Extended{} ->+ parsingError "extended reserved predicates are not supported"++decodeEquality :: TPTP.Sign -> Term -> Term -> Signed Literal+decodeEquality s a b = Signed (decodeSign s) (Equality a b)++-- | Encode a logical connective in TPTP.+encodeConnective :: Connective -> TPTP.Connective+encodeConnective = \case+ And -> TPTP.Conjunction+ Or -> TPTP.Disjunction+ Implies -> TPTP.Implication+ Equivalent -> TPTP.Equivalence+ Xor -> TPTP.ExclusiveOr++decodeConnected :: TPTP.Connective -> Formula -> Formula -> Formula+decodeConnected = \case+ TPTP.Conjunction -> Connected And+ TPTP.Disjunction -> Connected Or+ TPTP.Implication -> Connected Implies+ TPTP.Equivalence -> Connected Equivalent+ TPTP.ExclusiveOr -> Connected Xor+ TPTP.NegatedConjunction -> Negate .: Connected And+ TPTP.NegatedDisjunction -> Negate .: Connected Or+ TPTP.ReversedImplication -> flip (Connected Implies)+ where+ (.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d+ (.:) = (.) . (.)++-- | Encode a quantifier in TPTP.+encodeQuantifier :: Quantifier -> TPTP.Quantifier+encodeQuantifier = \case+ Forall -> TPTP.Forall+ Exists -> TPTP.Exists++-- | Decode a quantifier from TPTP.+decodeQuantifier :: TPTP.Quantifier -> Quantifier+decodeQuantifier = \case+ TPTP.Forall -> Forall+ TPTP.Exists -> Exists++-- | Encode a formula in unsorted first-order logic in TPTP.+encodeFormula :: Formula -> TPTP.UnsortedFirstOrder+encodeFormula = \case+ Atomic l -> TPTP.Atomic (encodeLiteral l)+ Negate f -> TPTP.Negated (encodeFormula f)+ Connected c f g -> TPTP.Connected (encodeFormula f) (encodeConnective c) (encodeFormula g)+ Quantified q v f -> TPTP.quantified (encodeQuantifier q) [(encodeVar v, TPTP.Unsorted ())] (encodeFormula f)++-- | Decode a formula in unsorted first-order logic from TPTP.+decodeFormula :: TPTP.UnsortedFirstOrder -> Partial Formula+decodeFormula = evalEnumerationT . decodeFormulaS++decodeFormulaS :: TPTP.UnsortedFirstOrder -> Substitutions Formula+decodeFormulaS = \case+ TPTP.Atomic l -> liftSignedLiteral <$> decodeLiteral l+ TPTP.Negated f -> Negate <$> decodeFormulaS f+ TPTP.Connected f c g -> decodeConnected c+ <$> decodeFormulaS f <*> decodeFormulaS g+ TPTP.Quantified q vs f -> foldr (curry $ quantified (decodeQuantifier q))+ <$> decodeFormulaS f <*> traverse (enumerate . fst) vs++-- | Encode a formula in unsorted first-order logic in TPTP.+encode :: LogicalExpression -> TPTP.Formula+encode = \case+ Clause c -> TPTP.CNF (encodeClause c)+ Formula f -> TPTP.FOF (encodeFormula f)++-- | Decode a formula in unsorted first-order logic from TPTP.+decode :: TPTP.Formula -> Partial LogicalExpression+decode = \case+ TPTP.FOF f -> Formula <$> decodeFormula f+ TPTP.CNF c -> Clause <$> decodeClause c+ TPTP.TFF0 f | Just g <- TPTP.unsortFirstOrder f -> Formula <$> decodeFormula g+ TPTP.TFF0{} -> parsingError "formulas in TFF0 are not supported"+ TPTP.TFF1{} -> parsingError "formulas in TFF1 are not supported"++-- | Encode a clause in unsorted first-order logic in TPTP.+encodeClause :: Clause -> TPTP.Clause+encodeClause = TPTP.clause . fmap encodeSignedLiteral . getLiterals++-- | Decode a clause in unsorted first-order logic from TPTP.+decodeClause :: TPTP.Clause -> Partial Clause+decodeClause = evalEnumerationT . decodeClauseS++decodeClauseS :: TPTP.Clause -> Substitutions Clause+decodeClauseS (TPTP.Clause ls) = Literals <$> traverse decodeSignedLiteralS (NE.toList ls)++encodeSign :: Sign -> TPTP.Sign+encodeSign = \case+ Positive -> TPTP.Positive+ Negative -> TPTP.Negative++decodeSign :: TPTP.Sign -> Sign+decodeSign = \case+ TPTP.Positive -> Positive+ TPTP.Negative -> Negative++encodeSignedLiteral :: Signed Literal -> (TPTP.Sign, TPTP.Literal)+encodeSignedLiteral (Signed s l) = (encodeSign s, encodeLiteral l)++decodeSignedLiteralS :: (TPTP.Sign, TPTP.Literal) -> Substitutions (Signed Literal)+decodeSignedLiteralS (s, l) = sign (decodeSign s) <$> decodeLiteral l++-- | Encode a set of first-order clauses in TPTP.+encodeClauses :: Clauses -> TPTP.TPTP+encodeClauses (Clauses cs) = TPTP.TPTP units+ where+ units = zipWith unit [1..] cs+ unit n f = TPTP.Unit (Right n) (clauze f) Nothing+ clauze = TPTP.Formula (TPTP.Standard TPTP.Axiom) . encode . Clause++-- | Encode a theorem in unsorted first-order logic in TPTP.+encodeTheorem :: Theorem -> TPTP.TPTP+encodeTheorem (Theorem as c) = TPTP.TPTP units+ where+ units = unit TPTP.Conjecture 0 c : zipWith (unit TPTP.Axiom) [1..] as+ unit r n f = TPTP.Unit (Right n) (formula r f) Nothing+ formula r = TPTP.Formula (TPTP.Standard r) . encode . Formula . close++-- | Decode a solution from a TSTP output.+decodeSolution :: TPTP.TSTP -> Partial Solution+decodeSolution (TPTP.TSTP szs units)+ | TPTP.SZS (Just (Right status)) _dataform <- szs = if+ | isProof status -> Proof <$> decodeRefutation units+ | isSaturation status -> Saturation <$> decodeDerivation units+ | otherwise -> parsingError $ "unsupported SZS " <> show status+ | otherwise = proofError "malformed input: missing SZS ontologies"++isProof :: TPTP.Success -> Bool+isProof = \case+ TPTP.UNS -> True+ TPTP.THM -> True+ _ -> False++isSaturation :: TPTP.Success -> Bool+isSaturation = \case+ TPTP.SAT -> True+ TPTP.CSA -> True+ _ -> False++decodeRefutation :: [TPTP.Unit] -> Partial (Refutation Integer)+decodeRefutation units = do+ derivation <- decodeDerivation units+ case unliftRefutation derivation of+ Just refutation -> return refutation+ Nothing -> proofError "malformed input: refutation not found"++decodeDerivation :: [TPTP.Unit] -> Partial (Derivation Integer)+decodeDerivation units = do+ decodedSequents <- traverse decodeSequent units+ let expressions = labeling decodedSequents+ return . evalEnumeration+ . foldM (decodeSequentS expressions) mempty+ $ decodedSequents++decodeSequentS :: Ord n => Map n LogicalExpression -> Derivation Integer ->+ Sequent n -> Enumeration n (Derivation Integer)+decodeSequentS es d s@(Sequent l i) =+ case find synonymous (antecedents i) of+ Just a -> alias l a $> d+ Nothing -> addSequent d <$> traverse enumerate s+ where synonymous a = es ! a ~= consequent i++decodeSequent :: TPTP.Unit -> Partial (Sequent TPTP.UnitName)+decodeSequent = \case+ TPTP.Unit name (TPTP.Formula (TPTP.Standard TPTP.Axiom) formula) Nothing -> do+ expression <- decode formula+ return $ Sequent name (Inference Axiom expression)+ TPTP.Unit name (TPTP.Formula role formula) (Just (source, _)) -> do+ rule <- decodeRule source role (collectParents source)+ expression <- decode formula+ return $ Sequent name (Inference rule expression)+ _ -> proofError "malformed input: unexpected unit"++collectParents :: TPTP.Source -> [TPTP.UnitName]+collectParents = \case+ TPTP.File{} -> []+ TPTP.Theory{} -> []+ TPTP.Creator{} -> []+ TPTP.Introduced{} -> []+ TPTP.Inference _ _ ps -> concatMap (\(TPTP.Parent p _) -> collectParents p) ps+ TPTP.UnitSource p -> [p]+ TPTP.UnknownSource -> []++decodeRule :: TPTP.Source -> TPTP.Reserved TPTP.Role -> [f] -> Partial (Rule f)+decodeRule s role as = case s of+ TPTP.Theory{} -> parsingError $ "unsupported unit source " ++ show s+ TPTP.Creator{} -> parsingError $ "unsupported unit source " ++ show s+ TPTP.UnitSource{} -> return $ Other "triviality" as+ TPTP.Introduced taut _ -> return $ decodeTautologyRule taut+ TPTP.UnknownSource -> return $ Unknown as+ TPTP.File{} -> decodeIntroductionRule role as+ TPTP.Inference rule _ _ -> return $ decodeInferenceRule rule as++decodeTautologyRule :: TPTP.Reserved TPTP.Intro -> Rule f+decodeTautologyRule = \case+ TPTP.Standard TPTP.ByAxiomOfChoice -> AxiomOfChoice+ TPTP.Extended "choice_axiom" -> AxiomOfChoice+ _ -> Axiom++decodeIntroductionRule :: TPTP.Reserved TPTP.Role -> [a] -> Partial (Rule f)+decodeIntroductionRule role as = case (role, as) of+ (TPTP.Standard TPTP.Axiom, []) -> return Axiom+ (TPTP.Standard TPTP.Conjecture, []) -> return Conjecture+ _ -> proofError $ "unexpected unit role " <> show role++decodeInferenceRule :: TPTP.Atom -> [f] -> Rule f+decodeInferenceRule (TPTP.Atom rule) as = case (rule, as) of+ ("negated_conjecture", [f]) -> NegatedConjecture f+ ("assume_negation", [f]) -> NegatedConjecture f+ ("flattening", [f]) -> Flattening f+ ("skolemisation", [f]) -> Skolemisation f+ ("skolemize", [f]) -> Skolemisation f+ ("ennf_transformation", [f]) -> EnnfTransformation f+ ("nnf_transformation", [f]) -> NnfTransformation f+ ("cnf_transformation", [f]) -> Clausification f+ ("trivial_inequality_removal", [f]) -> TrivialInequality f+ ("superposition", [f, g]) -> Superposition f g+ ("resolution", [f, g]) -> Resolution f g+ ("pm", [f, g]) -> Paramodulation f g+ ("subsumption_resolution", [f, g]) -> SubsumptionResolution f g+ ("forward_demodulation", [f, g]) -> ForwardDemodulation f g+ ("backward_demodulation", [f, g]) -> BackwardDemodulation f g+ _ -> Other (RuleName rule) as
+ src/ATP/Error.hs view
@@ -0,0 +1,95 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DeriveTraversable #-}++{-|+Module : ATP.Error+Description : Monads and monad transformers for computations with errors.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental++Monads and monad transformers for computations with errors.+-}++module ATP.Error (+ Error(..),+ Partial,+ PartialT(..),+ liftPartial,+ isSuccess,+ isFailure,+ exitCodeError,+ timeLimitError,+ memoryLimitError,+ parsingError,+ proofError,+ otherError+) where++import Control.Monad.Except (MonadTrans, ExceptT(..), MonadError(..), runExcept)+import Data.Either (isLeft, isRight)+import Data.Functor.Identity (Identity)+import Data.Text (Text)+import qualified Data.Text as T (pack)+++-- | The error that might occur while reconstructing the proof.+data Error+ = ExitCodeError Int Text+ -- ^ The theorem prover terminated with a non-zero exit code.+ | TimeLimitError+ -- ^ The theorem prover reached the time limit without producing a solution.+ | MemoryLimitError+ -- ^ The theorem prover reached the memory limit without producing a solution.+ | ParsingError Text+ -- ^ The output of the theorem prover is not a well-formed TSTP.+ | ProofError Text+ -- ^ The proof returned by the theorem prover is not well-formed.+ | OtherError Text+ -- ^ An uncategorized error.+ deriving (Show, Eq, Ord)++-- | The type of computations that might fail with an @'Error'@.+type Partial = PartialT Identity++-- | A monad transformer that adds failing with an @'Error'@ to other monads.+newtype PartialT m a = PartialT {+ runPartialT :: ExceptT Error m a+} deriving (Show, Eq, Ord, Functor, Applicative, Monad, MonadTrans, MonadError Error)++-- | Extractor for computations in the @'Partial'@ monad.+liftPartial :: Partial a -> Either Error a+liftPartial = runExcept . runPartialT++-- | Check whether a partial computation resulted successfully.+isSuccess :: Partial a -> Bool+isSuccess = isRight . liftPartial++-- | Check whether a partial computation resulted with an error.+isFailure :: Partial a -> Bool+isFailure = isLeft . liftPartial++-- | A smart constructor for a computation failed with an @'ExitCodeError'@.+exitCodeError :: Monad m => Int -> Text -> PartialT m a+exitCodeError exitCode err = PartialT (throwError $ ExitCodeError exitCode err)++-- | A smart constructor for a computation failed with a @'TimeLimitError'@.+timeLimitError :: Monad m => PartialT m a+timeLimitError = PartialT (throwError TimeLimitError)++-- | A smart constructor for a computation failed with a @'MemoryLimitError'@.+memoryLimitError :: Monad m => PartialT m a+memoryLimitError = PartialT (throwError MemoryLimitError)++-- | A smart constructor for a computation failed with a @'ParsingError'@.+parsingError :: Monad m => String -> PartialT m a+parsingError = PartialT . throwError . ParsingError . T.pack++-- | A smart constructor for a computation failed with a @'ProofError'@.+proofError :: Monad m => String -> PartialT m a+proofError = PartialT . throwError . ProofError . T.pack++-- | A smart constructor for a computation failed with a @'OtherError'@.+otherError :: Monad m => String -> PartialT m a+otherError = PartialT . throwError . OtherError . T.pack
+ src/ATP/FOL.hs view
@@ -0,0 +1,29 @@+{-|+Module : ATP.FOL+Description : Syntax of first-order logic.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental++Data structures that represent formulas and theorems in first-order logic,+and smart constructors for them.+-}++module ATP.FOL (+ module ATP.FirstOrder.Core,+ module ATP.FirstOrder.Alpha,+ module ATP.FirstOrder.Smart,+ module ATP.FirstOrder.Simplification,+ module ATP.FirstOrder.Occurrence,+ module ATP.FirstOrder.Conversion,+ module ATP.FirstOrder.Derivation+) where++import ATP.FirstOrder.Core+import ATP.FirstOrder.Alpha+import ATP.FirstOrder.Smart+import ATP.FirstOrder.Simplification+import ATP.FirstOrder.Occurrence+import ATP.FirstOrder.Conversion+import ATP.FirstOrder.Derivation
+ src/ATP/FirstOrder/Alpha.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++{-|+Module : ATP.FirstOrder.Alpha+Description : Monads and monad transformers for computations with free and+ bound variables.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module ATP.FirstOrder.Alpha (+ AlphaT,+ evalAlphaT,+ Alpha,+ evalAlpha,+ lookup,+ scope,+ enter,+ share,+ MonadAlpha(..)+) where++import Prelude hiding (lookup)+import Control.Applicative ((<|>))+import Control.Monad.Trans (MonadTrans(..))+import Control.Monad.Reader (MonadReader(..), ReaderT(..), asks)+import Control.Monad.State (MonadState(..), StateT(..), modify, gets)+import Data.Functor.Identity (Identity(..))+import qualified Data.List as L (lookup)+import qualified Data.Map as M (empty, lookup, insert, elems)+import Data.Map (Map)++import ATP.FirstOrder.Core+++-- | The stack of renamings for the bound variables in the expression.+type Stack = [(Var, Var)]++-- | The rename mapping for the free variables in the expression.+type Global = Map Var Var++-- | The monad transformer that adds to the given monad @m@ the ability to track+-- a renaming of free and bound variables in a first-order expression.+newtype AlphaT m a = AlphaT (ReaderT Stack (StateT Global m) a)+ deriving (Functor, Applicative, Monad, MonadReader Stack, MonadState Global)++instance MonadTrans AlphaT where+ lift = AlphaT . lift . lift++runAlphaT :: AlphaT m a -> m (a, Global)+runAlphaT (AlphaT r) = runStateT (runReaderT r []) M.empty++-- | Evaluate an alpha computation and return the final value,+-- discarding the global scope.+evalAlphaT :: Monad m => AlphaT m a -> m a+evalAlphaT = fmap fst . runAlphaT+++-- | The alpha monad parametrized by the type @a@ of the return value.+type Alpha a = AlphaT Identity a++-- | Evaluate an 'Alpha' computation and return the final value,+-- discarding the final variable renaming.+evalAlpha :: Alpha a -> a+evalAlpha = runIdentity . evalAlphaT+++-- | Lookup a variable, first in the stack of bound variables,+-- then in the global scope.+lookup :: Monad m => Var -> AlphaT m (Maybe Var)+lookup v = do+ bv <- asks (L.lookup v)+ fv <- gets (M.lookup v)+ return (bv <|> fv)++-- | Read the set of free and bound variables of the given 'AlphaT' computation.+scope :: Monad m => AlphaT m [Var]+scope = do+ bv <- asks (fmap snd)+ fv <- gets M.elems+ return (bv ++ fv)++-- | Run a computation inside 'AlphaT' with the variable renaming.+enter :: Monad m => Var -> Var -> AlphaT m a -> AlphaT m a+enter v w = local ((v,w):)++-- | Update the global scope with a variable renaming.+share :: Monad m => Var -> Var -> AlphaT m ()+share v w = modify (M.insert v w)+++-- | A helper monad for computations on free and bound occurrences of variables.+class Monad m => MonadAlpha m where+ -- | A monadic action to perform on a variable under a quantifier.+ binding :: Var -> AlphaT m Var++ -- | A monadic action to perform on a variable occurrence.+ occurrence :: Var -> AlphaT m Var
+ src/ATP/FirstOrder/Conversion.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE LambdaCase #-}++{-|+Module : ATP.FirstOrder.Conversion+Description : Conversions between first-order expressions.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module ATP.FirstOrder.Conversion (+ -- * Conversions+ -- ** Formulas+ liftSignedLiteral,+ unliftSignedLiteral,+ liftClause,+ unliftClause,++ -- ** Proofs+ liftContradiction,+ unliftContradiction,+ liftRefutation,+ unliftRefutation+) where++import qualified Data.Map as M (partition, toList)++import ATP.FirstOrder.Core+import ATP.FirstOrder.Derivation+import ATP.FirstOrder.Occurrence+++-- * Conversions++-- ** Formulas++-- | Convert a clause to a full first-order formula.+liftClause :: Clause -> Formula+liftClause = \case+ EmptyClause -> Falsity+ Literals ls -> close . foldl1 (Connected Or) . fmap liftSignedLiteral $ ls++-- | Try to convert a first-order formula /f/ to a clause.+-- This function succeeds if /f/ is a tree of disjunctions of+-- (negated) atomic formula.+unliftClause :: Formula -> Maybe Clause+unliftClause = unlift . unprefix+ where+ unlift = \case+ Connected Or f g -> mappend <$> unlift f <*> unlift g+ f -> UnitClause <$> unliftSignedLiteral f++-- | Convert a signed literal to a (negated) atomic formula.+liftSignedLiteral :: Signed Literal -> Formula+liftSignedLiteral (Signed s l) = case s of+ Positive -> Atomic l+ Negative -> Negate (Atomic l)++-- | Try to convert a first-order formula /f/ to a signed literal.+-- This function succeeds if /f/ is a (negated) atomic formula.+unliftSignedLiteral :: Formula -> Maybe (Signed Literal)+unliftSignedLiteral = \case+ Atomic l -> Just (Signed Positive l)+ Negate f -> sign Negative <$> unliftSignedLiteral f+ _ -> Nothing+++-- ** Proofs++-- | Convert a contradiction to an inference.+liftContradiction :: Contradiction f -> Inference f+liftContradiction (Contradiction r) = Inference r (Formula Falsity)++-- | Try to convert an inference to a contradiction.+unliftContradiction :: Inference f -> Maybe (Contradiction f)+unliftContradiction (Inference r e)+ | isContradiction e = Just (Contradiction r)+ | otherwise = Nothing++-- | Check whether a given expression is either a falsity or an empty clause.+isContradiction :: LogicalExpression -> Bool+isContradiction = \case+ Clause c | Falsity <- liftClause c -> True+ Formula Falsity -> True+ _ -> False++-- | Convert a refutation to a derivation.+liftRefutation :: Ord f => f -> Refutation f -> Derivation f+liftRefutation f (Refutation d c) = addSequent d (Sequent f (liftContradiction c))++-- | Try to convert a derivation to a refutation.+-- This function succeds if the derivation has exactly one inference+-- resulting in contradiction.+unliftRefutation :: Derivation f -> Maybe (Refutation f)+unliftRefutation (Derivation is) = Refutation (Derivation is') <$> c+ where+ (cs, is') = M.partition (isContradiction . consequent) is+ c | [(_, Inference r _)] <- M.toList cs = Just (Contradiction r)+ | otherwise = Nothing
+ src/ATP/FirstOrder/Core.hs view
@@ -0,0 +1,382 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++{-|+Module : ATP.FirstOrder.Core+Description : Data types representing unsorted first-order logic.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module ATP.FirstOrder.Core (+ -- * First-order logic+ Var,+ FunctionSymbol(..),+ Term(..),+ PredicateSymbol(..),+ Literal(..),+ Sign(..),+ Signed(..),+ sign,+ Clause(..),+ Clauses(..),+ Connective(..),+ isAssociative,+ Quantifier(..),+ Formula(..),+ LogicalExpression(..),+ Theorem(..),++ -- * Syntactic sugar+ -- $sugar+ Function,+ Constant,+ UnaryFunction,+ BinaryFunction,+ TernaryFunction,+ pattern Constant,+ pattern UnaryFunction,+ pattern BinaryFunction,+ pattern TernaryFunction,++ Predicate,+ Proposition,+ UnaryPredicate,+ BinaryPredicate,+ TernaryPredicate,+ pattern Proposition,+ pattern UnaryPredicate,+ pattern BinaryPredicate,+ pattern TernaryPredicate,++ pattern TautologyLiteral,+ pattern FalsityLiteral,++ pattern EmptyClause,+ pattern UnitClause,+ pattern TautologyClause,++ pattern NoClauses,+ pattern SingleClause,++ pattern Tautology,+ pattern Falsity,++ pattern Claim+) where++#if !MIN_VERSION_base(4, 11, 0)+import Data.Semigroup (Semigroup(..))+#endif+import Data.String (IsString(..))+import Data.Text (Text)+++-- * First-order logic++-- | The type of variables in first-order formulas.+type Var = Integer++-- | The type of function symbols in first-order formulas.+newtype FunctionSymbol = FunctionSymbol Text+ deriving (Show, Eq, Ord, IsString)++-- | The term in first-order logic.+data Term+ = Variable Var+ -- ^ A quantified variable.+ | Function FunctionSymbol [Term]+ -- ^ Application of a function symbol. The empty list of arguments+ -- represents a constant.+ deriving (Show, Eq, Ord)++-- | The type of predicate symbols in first-order formulas.+newtype PredicateSymbol = PredicateSymbol Text+ deriving (Show, Eq, Ord, IsString)++-- | The literal in first-order logic.+data Literal+ = Propositional Bool+ -- ^ A logical constant - tautology or falsum.+ | Predicate PredicateSymbol [Term]+ -- ^ Application of a predicate symbol. The empty list of arguments+ -- represents a boolean constant.+ | Equality Term Term+ -- ^ Equality between terms.+ deriving (Show, Eq, Ord)++-- | The sign of a logical expression is either positive or negative.+data Sign+ = Positive+ | Negative+ deriving (Eq, Show, Ord, Enum, Bounded)++instance Semigroup Sign where+ Negative <> Positive = Negative+ Positive <> Negative = Negative+ Negative <> Negative = Positive+ Positive <> Positive = Positive++instance Monoid Sign where+ mempty = Positive+ mappend = (<>)++-- | A signed expression is that annotated with a 'Sign'.+data Signed e = Signed {+ signof :: Sign,+ unsign :: e+} deriving (Eq, Show, Ord, Functor, Foldable, Traversable)++-- | Juxtapose a given signed expression with a given sign.+sign :: Sign -> Signed e -> Signed e+sign s (Signed z e) = Signed (s <> z) e++instance Applicative Signed where+ pure = Signed Positive+ Signed s f <*> e = sign s (fmap f e)++instance Monad Signed where+ Signed s e >>= f = sign s (f e)++-- | The first-order clause - an implicitly universally-quantified disjunction+-- of positive or negative literals, represented as a list of signed literals.+-- The empty clause is logically equivalent to falsum.+newtype Clause = Literals { getLiterals :: [Signed Literal] }+ deriving (Show, Eq, Ord, Semigroup, Monoid)++-- | A clause set is zero or more first-order clauses.+-- The empty clause set is logically equivalent to tautology.+newtype Clauses = Clauses { getClauses :: [Clause] }+ deriving (Show, Eq, Ord, Semigroup, Monoid)++-- | The quantifier in first-order logic.+data Quantifier+ = Forall -- ^ The universal quantifier.+ | Exists -- ^ The existential quantifier.+ deriving (Eq, Show, Ord, Enum, Bounded)++-- | The binary logical connective.+data Connective+ = And -- ^ Conjunction.+ | Or -- ^ Disjunction.+ | Implies -- ^ Implication.+ | Equivalent -- ^ Equivalence.+ | Xor -- ^ Exclusive or.+ deriving (Show, Eq, Ord, Enum, Bounded)++-- | Associativity of a given binary logical connective.+--+-- >>> isAssociative Implies+-- False+--+-- >>> isAssociative And+-- True+isAssociative :: Connective -> Bool+isAssociative = \case+ And -> True+ Or -> True+ Implies -> False+ Equivalent -> True+ Xor -> True++-- | The formula in first-order logic.+data Formula+ = Atomic Literal+ | Negate Formula+ | Connected Connective Formula Formula+ | Quantified Quantifier Var Formula+ deriving (Show, Eq, Ord)++-- | A logical expression is either a clause or a formula.+data LogicalExpression+ = Clause Clause+ | Formula Formula+ deriving (Show, Eq, Ord)++-- | A theorem is zero or more axioms and a conjecture.+data Theorem = Theorem {+ axioms :: [Formula],+ conjecture :: Formula+} deriving (Show, Eq, Ord)+++-- * Syntactic sugar++-- $sugar+--+-- Instances, type synonyms and pattern synonyms for syntactic convenience.++instance IsString Term where+ fromString = Constant . fromString++instance IsString Literal where+ fromString = flip Predicate [] . fromString++instance IsString e => IsString (Signed e) where+ fromString = Signed Positive . fromString++instance IsString Clause where+ fromString = UnitClause . fromString++instance IsString Formula where+ fromString = Proposition . fromString+++-- ** Function symbols++-- | The type of a function symbol - a mapping from zero or more terms+-- to a term.+type Function = [Term] -> Term++-- | The type of a constant symbol.+type Constant = Term++-- | The type of a function symbol with one argument.+type UnaryFunction = Term -> Term++-- | The type of a function symbol with two arguments.+type BinaryFunction = Term -> Term -> Term++-- | The type of a function symbol with three arguments.+type TernaryFunction = Term -> Term -> Term -> Term++-- | Build a proposition from a predicate symbol.+#if __GLASGOW_HASKELL__ == 800+pattern Constant :: FunctionSymbol -> Term+#else+pattern Constant :: FunctionSymbol -> Constant+#endif+pattern Constant f = Function f []++-- | Build a unary function from a function symbol.+#if __GLASGOW_HASKELL__ == 800+pattern UnaryFunction :: FunctionSymbol -> Term -> Term+#else+pattern UnaryFunction :: FunctionSymbol -> UnaryFunction+#endif+pattern UnaryFunction f a = Function f [a]++-- | Build a binary function from a function symbol.+#if __GLASGOW_HASKELL__ == 800+pattern BinaryFunction :: FunctionSymbol -> Term -> Term -> Term+#else+pattern BinaryFunction :: FunctionSymbol -> BinaryFunction+#endif+pattern BinaryFunction f a b = Function f [a, b]++-- | Build a ternary function from a function symbol.+#if __GLASGOW_HASKELL__ == 800+pattern TernaryFunction :: FunctionSymbol -> Term -> Term -> Term -> Term+#else+pattern TernaryFunction :: FunctionSymbol -> TernaryFunction+#endif+pattern TernaryFunction f a b c = Function f [a, b, c]+++-- ** Predicate symbols++-- | The type of a predicate symbol - a mapping from zero or more terms+-- to a formula.+type Predicate = [Term] -> Formula++-- | The type of a proposition.+type Proposition = Formula++-- | The type of a predicate symbol with one argument.+type UnaryPredicate = Term -> Formula++-- | The type of a predicate symbol with two arguments.+type BinaryPredicate = Term -> Term -> Formula++-- | The type of a function symbol with three arguments.+type TernaryPredicate = Term -> Term -> Term -> Formula++-- | Build a proposition from a predicate symbol.+#if __GLASGOW_HASKELL__ == 800+pattern Proposition :: PredicateSymbol -> Formula+#else+pattern Proposition :: PredicateSymbol -> Proposition+#endif+pattern Proposition p = Atomic (Predicate p [])++-- | Build a unary predicate from a predicate symbol.+#if __GLASGOW_HASKELL__ == 800+pattern UnaryPredicate :: PredicateSymbol -> Term -> Formula+#else+pattern UnaryPredicate :: PredicateSymbol -> UnaryPredicate+#endif+pattern UnaryPredicate p a = Atomic (Predicate p [a])++-- | Build a binary predicate from a predicate symbol.+#if __GLASGOW_HASKELL__ == 800+pattern BinaryPredicate :: PredicateSymbol -> Term -> Term -> Formula+#else+pattern BinaryPredicate :: PredicateSymbol -> BinaryPredicate+#endif+pattern BinaryPredicate p a b = Atomic (Predicate p [a, b])++-- | Build a ternary predicate from a predicate symbol.+#if __GLASGOW_HASKELL__ == 800+pattern TernaryPredicate :: PredicateSymbol -> Term -> Term -> Term -> Formula+#else+pattern TernaryPredicate :: PredicateSymbol -> TernaryPredicate+#endif+pattern TernaryPredicate p a b c = Atomic (Predicate p [a, b, c])+++-- ** Literals++-- | The positive tautology literal.+pattern TautologyLiteral :: Signed Literal+pattern TautologyLiteral = Signed Positive (Propositional True)++-- | The positive falsity literal.+pattern FalsityLiteral :: Signed Literal+pattern FalsityLiteral = Signed Positive (Propositional False)+++-- ** Clauses++-- | A unit clause with a single positive tautology literal.+-- 'TautologyClause' is semantically (but not syntactically) equivalent to+-- 'Tautology'.+pattern TautologyClause :: Clause+pattern TautologyClause = UnitClause TautologyLiteral++-- | The empty clause.+-- 'EmptyClause' is semantically (but not syntactically) equivalent to 'Falsity'.+pattern EmptyClause :: Clause+pattern EmptyClause = Literals []++-- | The unit clause.+pattern UnitClause :: Signed Literal -> Clause+pattern UnitClause l = Literals [l]++-- | The set of clauses with a single clause in it.+pattern NoClauses :: Clauses+pattern NoClauses = Clauses []++-- | The set of clauses with a single clause in it.+pattern SingleClause :: Clause -> Clauses+pattern SingleClause c = Clauses [c]+++-- ** Formulas++-- | The logical tautology.+pattern Tautology :: Formula+pattern Tautology = Atomic (Propositional True)++-- | The logical false.+-- 'Falsity' is semantically (but not syntactically) equivalent to 'EmptyClause'.+pattern Falsity :: Formula+pattern Falsity = Atomic (Propositional False)++-- | A logical claim is a conjecture entailed by the empty set of axioms.+pattern Claim :: Formula -> Theorem+pattern Claim f = Theorem [] f
+ src/ATP/FirstOrder/Derivation.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE CPP #-}++{-|+Module : ATP.FirstOrder.Derivation+Description : Derivations in first-order logic.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module ATP.FirstOrder.Derivation (+ -- * Proofs+ Rule(..),+ RuleName(..),+ ruleName,+ Inference(..),+ antecedents,+ Contradiction(..),+ Sequent(..),+ Derivation(..),+ addSequent,+ breadthFirst,+ labeling,+ Refutation(..),+ Solution(..)+) where++import Data.Foldable (toList)+import Data.Function (on)+import Data.List (sortBy)+import qualified Data.Map as M (fromList, insert, toList)+import Data.Map (Map, (!))+#if !MIN_VERSION_base(4, 11, 0)+import Data.Semigroup (Semigroup)+#endif+import Data.String (IsString(..))+import Data.Text (Text)++import ATP.FirstOrder.Core+++-- * Proofs++-- | The inference rule.+data Rule f+ = Axiom+ | Conjecture+ | NegatedConjecture f+ | Flattening f+ | Skolemisation f+ | EnnfTransformation f+ | NnfTransformation f+ | Clausification f+ | TrivialInequality f+ | Superposition f f+ | Resolution f f+ | Paramodulation f f+ | SubsumptionResolution f f+ | ForwardDemodulation f f+ | BackwardDemodulation f f+ | AxiomOfChoice+ | Unknown [f]+ | Other RuleName [f]+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++-- | The name of an inference rule.+newtype RuleName = RuleName { unRuleName :: Text }+ deriving (Show, Eq, Ord, IsString)++-- | The name of the given inference rule.+--+-- >>> unRuleName (ruleName AxiomOfChoice)+-- "axiom of choice"+ruleName :: Rule f -> RuleName+ruleName = \case+ Axiom{} -> "axiom"+ Conjecture{} -> "conjecture"+ NegatedConjecture{} -> "negated conjecture"+ Flattening{} -> "flattening"+ Skolemisation{} -> "skolemisation"+ EnnfTransformation{} -> "ennf transformation"+ NnfTransformation{} -> "nnf transformation"+ Clausification{} -> "clausification"+ TrivialInequality{} -> "trivial inequality"+ Superposition{} -> "superposition"+ Resolution{} -> "resolution"+ Paramodulation{} -> "paramodulation"+ SubsumptionResolution{} -> "subsumption resolution"+ ForwardDemodulation{} -> "forward demodulation"+ BackwardDemodulation{} -> "backward demodulation"+ AxiomOfChoice{} -> "axiom of choice"+ Unknown{} -> "unknown"+ Other name _ -> name++-- | A logical inference is an expression of the form+--+-- > A_1 ... A_n+-- > ----------- R,+-- > C+--+-- where each of @A_1@, ... @A_n@ (called the 'antecedents'), and @C@+-- (called the 'consequent') are formulas and @R@ is an inference 'Rule'.+data Inference f = Inference {+ inferenceRule :: Rule f,+ consequent :: LogicalExpression+} deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++-- | The antecedents of an inference.+antecedents :: Inference f -> [f]+antecedents = toList++-- | Contradiction is a special case of an inference that has the logical falsum+-- as the consequent.+newtype Contradiction f = Contradiction (Rule f)+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++-- | A sequent is a logical inference, annotated with a label.+-- Linked sequents form derivations.+data Sequent f = Sequent f (Inference f)+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++sequentMap :: Ord f => [Sequent f] -> Map f (Inference f)+sequentMap ss = M.fromList [(f, e) | Sequent f e <- ss]++-- | Construct a mapping between inference labels and their correspondent+-- formulas.+labeling :: Ord f => [Sequent f] -> Map f LogicalExpression+labeling = fmap consequent . sequentMap++-- | A derivation is a directed asyclic graph of logical inferences.+-- In this graph nodes are formulas and edges are inference rules.+-- The type parameter @f@ is used to label and index the nodes.+newtype Derivation f = Derivation (Map f (Inference f))+ deriving (Show, Eq, Ord, Semigroup, Monoid)++-- | Attach a sequent to a derivation.+addSequent :: Ord f => Derivation f -> Sequent f -> Derivation f+addSequent (Derivation m) (Sequent f i) = Derivation (M.insert f i m)++fromDerivation :: Derivation f -> [Sequent f]+fromDerivation (Derivation m) = fmap (uncurry Sequent) (M.toList m)++-- | Traverse the given derivation breadth-first and produce a list of sequents.+breadthFirst :: Ord f => Derivation f -> [Sequent f]+breadthFirst d = sortBy (compare `on` criteria) (fromDerivation d)+ where criteria (Sequent l (Inference r f)) = (distances d ! l, r, f)++distances :: Ord f => Derivation f -> Map f Integer+distances (Derivation m) = fmap distance m+ where+ distance i+ | null (antecedents i) = 0+ | otherwise = 1 + maximum (fmap (\a -> distance (m ! a)) (antecedents i))++-- | A refutation is a special case of a derivation that results in a+-- contradiction. A successful proof produces by an automated theorem prover+-- is a proof by refutation.+data Refutation f = Refutation (Derivation f) (Contradiction f)+ deriving (Show, Eq, Ord)++-- | The solution produced by an automated first-order theorem prover.+data Solution+ = Saturation (Derivation Integer)+ -- ^ A theorem can be disproven if the prover constructs a saturated set of+ -- first-order clauses.+ | Proof (Refutation Integer)+ -- ^ A theorem can be proven if the prover derives contradiction (the empty+ -- clause) from the set of axioms and the negated conjecture.+ deriving (Show, Eq, Ord)
+ src/ATP/FirstOrder/Occurrence.hs view
@@ -0,0 +1,295 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleInstances #-}++{-|+Module : ATP.FirstOrder.Occurrence+Description : Occurrences of variables in first-order expressions.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module ATP.FirstOrder.Occurrence (+ -- * Occurrence+ FirstOrder(..),+ closed,+ close,+ unprefix+) where++import Prelude hiding (lookup)+import Control.Monad (liftM2, zipWithM, when)+import Data.Function (on)+#if !MIN_VERSION_base(4, 11, 0)+import Data.Semigroup (Semigroup(..))+#endif+import qualified Data.Set as S (insert, delete, member, null, singleton)+import Data.Set (Set)++import ATP.FirstOrder.Core+import ATP.FirstOrder.Alpha++-- $setup+-- >>> :load Property.Generators+++-- * Occurrence++infix 5 ~=++-- | A class of first-order expressions, i.e. expressions that might contain+-- variables. @t'Formula'@s, @'Literal'@s and @'Term'@s are first-order expressions.+--+-- A variable can occur both as free and bound, therefore+-- @'free' e@ and @'bound' e@ are not necessarily disjoint and+-- @v `freeIn` e@ and @v `boundIn` e@ are not necessarily musually exclusive.+--+-- @'vars'@, @'free'@ and @'bound'@ are connected by the following property.+--+-- > free e <> bound e == vars e+--+-- @'occursIn'@, @'freeIn'@ and @'boundIn'@ are connected by the following property.+--+-- > v `freeIn` e || v `boundIn` e == v `occursIn` e+--+class FirstOrder e where+ -- | The set of all variables that occur anywhere in the given expression.+ vars :: e -> Set Var++ -- | The set of variables that occur freely in the given expression,+ -- i.e. are not bound by any quantifier inside the expression.+ free :: e -> Set Var++ -- | The set of variables that occur bound in the given expression,+ -- i.e. are bound by a quantifier inside the expression.+ bound :: e -> Set Var++ -- | Check whether the given variable occurs anywhere in the given expression.+ occursIn :: Var -> e -> Bool+ v `occursIn` e = v `S.member` vars e++ -- | Check whether the given variable occurs freely anywhere in the given expression.+ freeIn :: Var -> e -> Bool+ v `freeIn` e = v `S.member` free e++ -- | Check whether the given variable occurs bound anywhere in the given expression.+ boundIn :: Var -> e -> Bool+ v `boundIn` e = v `S.member` bound e++ -- | Check whether the given expression is ground, i.e. does not contain+ -- any variables.+ --+ -- Note that /ground formula/ is sometimes understood as /formula that does/+ -- /not contain any free variables/. In this library such formulas are called+ -- @'closed'@.+ ground :: e -> Bool+ ground = S.null . vars++ -- | Check whether two given expressions are alpha-equivalent, that is+ -- equivalent up to renaming of variables.+ --+ -- '(~=)' is an equivalence relation.+ --+ -- __Symmetry__+ --+ -- > e ~= e+ --+ -- __Reflexivity__+ --+ -- > a ~= b == b ~= a+ --+ -- __Transitivity__+ --+ -- > a ~= b && b ~= c ==> a ~= c+ --+ (~=) :: e -> e -> Bool+ a ~= b = evalAlpha (a ?= b)++ -- | A helper function calculating alpha-equivalence using the 'Alpha' monad stack.+ (?=) :: e -> e -> Alpha Bool++ alpha :: MonadAlpha m => e -> AlphaT m e++instance FirstOrder LogicalExpression where+ vars = \case+ Clause c -> vars c+ Formula f -> vars f++ free = \case+ Clause c -> free c+ Formula f -> free f++ bound = \case+ Clause c -> bound c+ Formula f -> bound f++ occursIn v = \case+ Clause c -> occursIn v c+ Formula f -> occursIn v f++ freeIn v = \case+ Clause c -> freeIn v c+ Formula f -> freeIn v f++ boundIn v = \case+ Clause c -> boundIn v c+ Formula f -> boundIn v f++ ground = \case+ Clause c -> ground c+ Formula f -> ground f++ Clause c ?= Clause c' = c ?= c'+ Formula f ?= Formula f' = f ?= f'+ _ ?= _ = return False++ alpha = \case+ Clause c -> Clause <$> alpha c+ Formula f -> Formula <$> alpha f++instance FirstOrder Formula where+ vars = \case+ Atomic l -> vars l+ Negate f -> vars f+ Connected _ f g -> vars f <> vars g+ Quantified _ _ f -> vars f++ free = \case+ Atomic l -> free l+ Negate f -> free f+ Connected _ f g -> free f <> free g+ Quantified _ v f -> S.delete v (free f)++ bound = \case+ Atomic{} -> mempty+ Negate f -> bound f+ Connected _ f g -> bound f <> bound g+ Quantified _ v f -> if v `freeIn` f then S.insert v (bound f) else bound f++ Atomic l ?= Atomic l' = l ?= l'+ Negate f ?= Negate f' = f ?= f'+ Connected c f g ?= Connected c' f' g' | c == c' = liftM2 (&&) (f ?= f') (g ?= g')+ Quantified q v f ?= Quantified q' v' f' | q == q' = enter v v' (f ?= f')+ _ ?= _ = return False++ alpha = \case+ Atomic l -> Atomic <$> alpha l+ Negate f -> Negate <$> alpha f+ Connected c f g -> Connected c <$> alpha f <*> alpha g+ Quantified q v f -> do+ v' <- binding v+ f' <- enter v v' (alpha f)+ return (Quantified q v' f')++instance FirstOrder Clause where+ vars = vars . getLiterals+ free = vars+ bound _ = mempty+ (~=) = (~=) `on` getLiterals+ (?=) = (?=) `on` getLiterals+ alpha = fmap Literals . traverse alpha . getLiterals++instance FirstOrder e => FirstOrder (Signed e) where+ vars = vars . unsign+ free = free . unsign+ bound = bound . unsign++ occursIn v = occursIn v . unsign+ freeIn v = freeIn v . unsign+ boundIn v = boundIn v . unsign++ ground = ground . unsign++ (~=) = (~=) `on` unsign+ (?=) = (?=) `on` unsign++ alpha = traverse alpha++instance FirstOrder Literal where+ vars = \case+ Propositional{} -> mempty+ Predicate _ ts -> vars ts+ Equality a b -> vars a <> vars b++ free = vars+ bound _ = mempty++ Propositional b ?= Propositional b' = return (b == b')+ Predicate p ts ?= Predicate p' ts' | p == p' = ts ?= ts'+ Equality a b ?= Equality a' b' = liftM2 (&&) (a ?= a') (b ?= b')+ _ ?= _ = return False++ alpha = \case+ Propositional b -> return (Propositional b)+ Predicate p ts -> Predicate p <$> traverse alpha ts+ Equality a b -> Equality <$> alpha a <*> alpha b++instance FirstOrder Term where+ vars = \case+ Variable v -> vars v+ Function _ ts -> vars ts++ free = vars+ bound _ = mempty++ Variable v ?= Variable v' = v ?= v'+ Function f ts ?= Function f' ts' | f == f' = ts ?= ts'+ _ ?= _ = return False++ alpha = \case+ Function f ts -> Function f <$> traverse alpha ts+ Variable v -> Variable <$> alpha v++instance FirstOrder Var where+ vars = S.singleton+ free = vars+ bound _ = mempty++ v ?= v' = lookup v >>= \case+ Just w' -> return (w' == v')+ Nothing -> do+ vs <- scope+ let f = v' `notElem` vs+ when f (share v v')+ return f++ alpha v = lookup v >>= \case+ Just v' -> occurrence v'+ Nothing -> do { v' <- binding v; share v v'; return v' }++instance FirstOrder e => FirstOrder [e] where+ vars = mconcat . fmap vars+ free = vars+ bound = mempty++ es ?= es' | length es == length es' = and <$> zipWithM (?=) es es'+ _ ?= _ = return False++ alpha = traverse alpha++-- | Check whether the given formula is closed, i.e. does not contain any free+-- variables.+closed :: Formula -> Bool+closed = S.null . free++-- | Make any given formula closed by adding a top-level universal quantifier+-- for each of its free variables.+--+-- @'close'@ and @'unprefix'@ are connected by the following property.+--+-- prop> unprefix (close f) === f+--+close :: Formula -> Formula+close f = foldl (flip $ Quantified Forall) f (free f)++-- | Remove the top-level quantifiers.+--+-- >>> unprefix (Quantified Forall 1 (Quantified Exists 2 (Atomic (Equality (Variable 1) (Variable 2)))))+-- Atomic (Equality (Variable 1) (Variable 2))+--+unprefix :: Formula -> Formula+unprefix = \case+ Quantified _ _ f -> unprefix f+ f -> f
+ src/ATP/FirstOrder/Simplification.hs view
@@ -0,0 +1,119 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-}++{-|+Module : ATP.FirstOrder.Simplification+Description : Simplification of first-order expressions.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}+module ATP.FirstOrder.Simplification (+ -- * Simplification+ Simplify(..)+) where++import ATP.FirstOrder.Core+import ATP.FirstOrder.Smart++-- $setup+-- >>> :set -XOverloadedStrings+-- >>> :load Property.Generators+++-- * Simplification++-- | A class of first-order expressions that 'simplify' syntactically shrinks+-- while preserving their evaluation.+class Simplify a where+ simplify :: a -> a++-- | Simplify the given formula by replacing each of its constructors with+-- corresponding smart constructors.+instance Simplify LogicalExpression where+ simplify = \case+ Clause c -> Clause (simplify c)+ Formula f -> Formula (simplify f)++-- | Simplify the given clause by replacing the 'Literals' constructor with+-- the smart constructor 'clause'. The effects of simplification are+-- the following.+--+-- * @'simplify' c@ does not contain negative constant literals.+-- * @'simplify' c@ does not contain falsum literals.+-- * @'simplify' c@ does not contain redundant tautology literals.+--+-- >>> simplify (UnitClause (Signed Negative (Propositional True)))+-- Literals {getLiterals = []}+--+-- >>> simplify (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])])+-- Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}+--+-- >>> simplify (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])])+-- Literals {getLiterals = [Signed {signof = Positive, unsign = Propositional True}]}+--+instance Simplify Clause where+ simplify = clause . getLiterals++-- | Simplify the given clause set by replacing the 'Clauses' constructor with+-- the smart constructor 'clauses'. The effects of simplification are+-- the following.+--+-- * @'simplify' c@ does not contain negative constant literals.+-- * @'simplify' c@ does not contain falsum literals.+-- * @'simplify' c@ does not contain tautology literals.+-- * @'simplify' c@ does not contain redundant falsum literals.+--+-- >>> simplify (SingleClause (UnitClause (Signed Negative (Propositional True))))+-- Clauses {getClauses = [Literals {getLiterals = []}]}+--+-- >>> simplify (SingleClause (Literals [FalsityLiteral, Signed Positive (Predicate "p" [])]))+-- Clauses {getClauses = [Literals {getLiterals = [Signed {signof = Positive, unsign = Predicate (PredicateSymbol "p") []}]}]}+--+-- >>> simplify (SingleClause (Literals [TautologyLiteral, Signed Positive (Predicate "p" [])]))+-- Clauses {getClauses = []}+--+instance Simplify Clauses where+ simplify = clauses . getClauses++-- | Simplify the given formula by replacing each of its constructors with+-- corresponding smart constructors. The effects of simplification are+-- the following.+--+-- * @'simplify' f@ does not contain nested negations.+-- * @'simplify' f@ does not contain some of the constant atomic formulas from @f@.+-- * All chained applications of any binary connective inside+-- @'simplify' f@ are right-associative.+--+-- Any formula built only using smart constructors is simplified by construction.+--+-- >>> simplify (Connected Or tautology (Atomic (Predicate "p" [])))+-- Atomic (Propositional True)+--+-- >>> simplify (Negate (Negate (Atomic (Predicate "p" []))))+-- Atomic (Predicate "p" [])+--+-- >>> simplify (Connected And (Connected And (Atomic (Predicate "p" [])) (Atomic (Predicate "q" []))) (Atomic (Predicate "r" [])))+-- Connected And (Atomic (Predicate "p" [])) (Connected And (Atomic (Predicate "q" [])) (Atomic (Predicate "r" [])))+--+instance Simplify Formula where+ simplify = \case+ Atomic l -> Atomic l+ Negate f -> neg (simplify f)+ Connected c f g -> simplify f # simplify g where (#) = smartConnective c+ Quantified q v f -> quantified q (v, simplify f)++-- | Convert a binary connective to its corresponding smart constructor.+smartConnective :: Connective -> Formula -> Formula -> Formula+smartConnective = \case+ And -> (/\)+ Or -> (\/)+ Implies -> (==>)+ Equivalent -> (<=>)+ Xor -> (<~>)++-- | Simplify the given theorem by flattening the conjunction of its premises+-- and its conjecture.+instance Simplify Theorem where+ simplify (Theorem as c) = flattenConjunction (fmap simplify as) |- simplify c
+ src/ATP/FirstOrder/Smart.hs view
@@ -0,0 +1,569 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE FlexibleInstances #-}++{-|+Module : ATP.FirstOrder.Smart+Description : Smart constructors for terms and formulas in first-order logic.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module ATP.FirstOrder.Smart (+ -- * Smart constructors+ signed,+ unitClause,+ clause,+ singleClause,+ clauses,+ (===),+ (=/=),+ neg,+ (\/),+ (/\),+ (==>),+ (<=>),+ (<~>),+ Binder(..),+ forall,+ exists,+ (|-),++ -- * Monoids+ Conjunction(..),+ conjunction,+ Disjunction(..),+ disjunction,+ Equivalence(..),+ equivalence,+ Inequivalence(..),+ inequivalence,++ -- * Miscellaneous+ flattenConjunction,+ flattenDisjunction+) where++import Data.Coerce (coerce)+import qualified Data.Foldable as Foldable (toList)+#if !MIN_VERSION_base(4, 11, 0)+import Data.Semigroup (Semigroup(..))+#endif++import ATP.FirstOrder.Core++-- $setup+-- >>> :set -XOverloadedStrings+-- >>> :load Property.Generators+-- >>> let eq = binaryPredicate "eq"+++-- * Smart constructors++infix 8 ===+infix 8 =/=+infixl 7 /\ --+infixl 6 \/+infixl 6 \./+infix 5 ==>+infixl 5 <=>+infixl 5 <~>+infix 2 |-++-- | A smart constructor for a signed literal.+signed :: Sign -> Literal -> Signed Literal+signed Negative (Propositional b) = Signed Positive (Propositional (not b))+signed s l = Signed s l++-- | A smart constructor for a unit clause.+unitClause :: Signed Literal -> Clause+unitClause (Signed s l) = case signed s l of+ FalsityLiteral -> EmptyClause+ sl -> UnitClause sl++-- | A smart contructor for a clause.+-- 'clause' eliminates negated boolean constants, falsums and redundant tautologies.+clause :: Foldable f => f (Signed Literal) -> Clause+clause = clauseUnion . fmap unitClause . Foldable.toList++-- | A smart constructor for a set of clauses with a single clause in it.+singleClause :: Clause -> Clauses+singleClause (Literals ls) = case clause ls of+ TautologyClause -> NoClauses+ c -> SingleClause c++-- | A smart constructor for the set of clauses.+-- 'clauses' eliminates negated boolean constants, falsums and redundant tautologies.+clauses :: Foldable f => f Clause -> Clauses+clauses = clauseConjunction . fmap singleClause . Foldable.toList++-- | A smart constructor for equality.+(===) :: Term -> Term -> Formula+a === b = Atomic (Equality a b)++-- | A smart constructor for inequality.+(=/=) :: Term -> Term -> Formula+a =/= b = Negate (a === b)++-- | A smart constructor for negation.+neg :: Formula -> Formula+neg = \case+ Tautology -> Falsity+ Falsity -> Tautology+ Negate f -> f+ f -> Negate f++-- | A smart contructor for the 'And' connective.+-- ('/\') has the following properties.+--+-- __Associativity__+--+-- prop> (f /\ g) /\ h == f /\ (g /\ h)+--+-- __Left identity__+--+-- prop> Tautology /\ g == g+--+-- __Right identity__+--+-- prop> f /\ Tautology == f+--+-- __Left zero__+--+-- prop> Falsity /\ g == Falsity+--+-- __Right zero__+--+-- prop> f /\ Falsity == Falsity+--+(/\) :: Formula -> Formula -> Formula+Falsity /\ _ = Falsity+Tautology /\ g = g+_ /\ Falsity = Falsity+f /\ Tautology = f+Connected And f g /\ h = f /\ (g /\ h)+f /\ g = Connected And f g++-- | A smart constructor for the 'Or' connective.+-- ('\/') has the following properties.+--+-- __Associativity__+--+-- prop> (f \/ g) \/ h == f \/ (g \/ h)+--+-- __Left identity__+--+-- prop> Falsity \/ g == g+--+-- __Right identity__+--+-- prop> f \/ Falsity == f+--+-- __Left zero__+--+-- prop> Tautology \/ g == Tautology+--+-- __Right zero__+--+-- prop> f \/ Tautology == Tautology+--+(\/) :: Formula -> Formula -> Formula+Tautology \/ _ = Tautology+Falsity \/ g = g+_ \/ Tautology = Tautology+f \/ Falsity = f+Connected Or f g \/ h = f \/ (g \/ h)+f \/ g = Connected Or f g++-- | A smart constructor for the 'Implies' connective.+(==>) :: Formula -> Formula -> Formula+Tautology ==> g = g+Falsity ==> _ = Tautology+_ ==> Tautology = Tautology+f ==> Falsity = neg f+f ==> g = Connected Implies f g++-- | A smart constructor for the 'Equivalent' connective.+-- ('<=>') has the following properties.+--+-- __Associativity__+--+-- prop> (f <=> g) <=> h == f <=> (g <=> h)+--+-- __Left identity__+--+-- prop> Tautology <=> g == g+--+-- __Right identity__+--+-- prop> f <=> Tautology == f+--+(<=>) :: Formula -> Formula -> Formula+Tautology <=> g = g+f <=> Tautology = f+Connected Equivalent f g <=> h = f <=> (g <=> h)+f <=> g = Connected Equivalent f g++-- | A smart constructor for the 'Xor' connective.+-- ('<~>') has the following properties.+--+-- __Associativity__+--+-- prop> (f <~> g) <~> h == f <~> (g <~> h)+--+-- __Left identity__+--+-- prop> Falsity <~> g == g+--+-- __Right identity__+--+-- prop> f <~> Falsity == f+--+(<~>) :: Formula -> Formula -> Formula+Falsity <~> g = g+f <~> Falsity = f+Connected Xor f g <~> h = f <~> (g <~> h)+f <~> g = Connected Xor f g++-- | A class of binders for quantified variables.+--+-- This class and its instances provides machinery for using polyvariadic+-- functions as higher-order abstract syntax for bindings of+-- quantified variables.+--+-- > eq = binaryPredicate "eq"+--+-- >>> quantified Forall $ \x -> x `eq` x+-- Quantified Forall 1 (Atomic (Predicate "eq" [Variable 1,Variable 1]))+--+-- >>> quantified Forall $ \x y -> x `eq` y ==> y `eq` x+-- Quantified Forall 2 (Quantified Forall 1 (Connected Implies (Atomic (Predicate "eq" [Variable 2,Variable 1])) (Atomic (Predicate "eq" [Variable 1,Variable 2]))))+class Binder b where+ -- | A smart constructor for quantified formulas.+ quantified :: Quantifier -> b -> Formula++-- | The degenerate instance - no variable is bound.+instance Binder Formula where+ quantified _ f = f++-- | The trivial instance - binder of the varible with the given name.+instance Binder (Var, Formula) where+ quantified q (v, f) = case f of+ Tautology -> f+ Falsity -> f+ _ -> Quantified q v f++-- | The recursive instance for polyvariadic bindings of quantified variables.+-- This is a generalized version of+-- <https://emilaxelsson.github.io/documents/axelsson2013using.pdf>.+instance Binder b => Binder (Term -> b) where+ quantified q b = quantified q (v, f)+ where+ f = quantified q (b (Variable v))+ v = 1 + maxvar f++ maxvar :: Formula -> Var+ maxvar = \case+ Atomic{} -> 0+ Negate g -> maxvar g+ Connected _ g h -> maxvar g `max` maxvar h+ Quantified _ w _ -> w++-- | A smart constructor for universally quantified formulas.+-- Provides a polyvariadic higher-order abstract syntax for the bindings of+-- universally quantified variables.+forall :: Binder b => b -> Formula+forall = quantified Forall++-- | A smart constructor for existentially quantified formulas.+-- Provides a polyvariadic higher-order abstract syntax for the bindings of+-- existentially quantified variables.+exists :: Binder b => b -> Formula+exists = quantified Exists++-- | A synonym for 'Theorem'.+(|-) :: Foldable f => f Formula -> Formula -> Theorem+as |- c = Theorem (Foldable.toList as) c+++-- * Monoids in first-order logic++-- | The ('Tautology', '/\') monoid.+newtype Conjunction = Conjunction { getConjunction :: Formula }+ deriving (Show, Eq, Ord)++instance Semigroup Conjunction where+ (<>) = coerce (/\)++instance Monoid Conjunction where+ mempty = Conjunction Tautology+ mappend = (<>)++-- | Build the conjunction of formulas in a list.+conjunction :: Foldable f => f Formula -> Formula+conjunction = getConjunction . mconcat . fmap Conjunction . Foldable.toList++-- | The ('Falsity', '\/') monoid.+newtype Disjunction = Disjunction { getDisjunction :: Formula }+ deriving (Show, Eq, Ord)++instance Semigroup Disjunction where+ (<>) = coerce (\/)++instance Monoid Disjunction where+ mempty = Disjunction Falsity+ mappend = (<>)++-- | Build the disjunction of formulas in a list.+disjunction :: Foldable f => f Formula -> Formula+disjunction = getDisjunction . mconcat . fmap Disjunction . Foldable.toList++-- | The ('Tautology', '<=>') monoid.+newtype Equivalence = Equivalence { getEquivalence :: Formula }+ deriving (Show, Eq, Ord)++instance Semigroup Equivalence where+ (<>) = coerce (<=>)++instance Monoid Equivalence where+ mempty = Equivalence Tautology+ mappend = (<>)++-- | Build the equivalence of formulas in a list.+equivalence :: Foldable f => f Formula -> Formula+equivalence = getEquivalence . mconcat . fmap Equivalence . Foldable.toList++-- | The ('Falsity', '<~>') monoid.+newtype Inequivalence = Inequivalence { getInequivalence :: Formula }+ deriving (Show, Eq, Ord)++instance Semigroup Inequivalence where+ (<>) = coerce (<~>)++instance Monoid Inequivalence where+ mempty = Inequivalence Falsity+ mappend = (<>)++-- | Build the inequivalence of formulas in a list.+inequivalence :: Foldable f => f Formula -> Formula+inequivalence = getInequivalence . mconcat . fmap Inequivalence . Foldable.toList+++-- * Miscellaneous++-- | Smart conjunction of two clauses.+-- ('/.\') has the following properties.+--+-- __Associativity__+--+-- prop> (f /.\ g) /.\ h == f /.\ (g /.\ h)+--+-- __Left identity__+--+-- prop> NoClauses /.\ g == g+--+-- __Right identity__+--+-- prop> f /.\ NoClauses == f+--+-- __Left zero__+--+-- prop> SingleClause EmptyClause /.\ g == SingleClause EmptyClause+--+-- __Right zero__+--+-- prop> f /.\ SingleClause EmptyClause == SingleClause EmptyClause+--+(/.\) :: Clauses -> Clauses -> Clauses+SingleClause EmptyClause /.\ _ = SingleClause EmptyClause+_ /.\ SingleClause EmptyClause = SingleClause EmptyClause+Clauses cs /.\ Clauses ss = Clauses (cs <> ss)++-- | The ('NoClauses', '/.\') monoid with the absorbing element 'SingleClause EmptyClause'.+newtype ClauseConjunction = ClauseConjunction { getClauseConjunction :: Clauses }+ deriving (Show, Eq, Ord)++instance Semigroup ClauseConjunction where+ (<>) = coerce (/.\)++instance Monoid ClauseConjunction where+ mempty = ClauseConjunction NoClauses+ mappend = (<>)++-- | Build the conjunction of a collection of clauses.+clauseConjunction :: Foldable f => f Clauses -> Clauses+clauseConjunction = getClauseConjunction . mconcat . fmap ClauseConjunction . Foldable.toList++-- | Smart union of two clauses.+-- ('\./') has the following properties.+--+-- __Associativity__+--+-- prop> (f \./ g) \./ h == f \./ (g \./ h)+--+-- __Left identity__+--+-- prop> EmptyClause \./ c == c+--+-- __Right identity__+--+-- prop> c \./ EmptyClause == c+--+-- __Left zero__+--+-- prop> TautologyClause \./ c == TautologyClause+--+-- __Right zero__+--+-- prop> c \./ TautologyClause == TautologyClause+--+(\./) :: Clause -> Clause -> Clause+TautologyClause \./ _ = TautologyClause+_ \./ TautologyClause = TautologyClause+Literals cs \./ Literals ss = Literals (cs <> ss)++-- | The ('EmptyClause', '\./') monoid with the absorbing element 'TautologyClause'.+newtype ClauseUnion = ClauseUnion { getClauseUnion :: Clause }+ deriving (Show, Eq, Ord)++instance Semigroup ClauseUnion where+ (<>) = coerce (\./)++instance Monoid ClauseUnion where+ mempty = ClauseUnion EmptyClause+ mappend = (<>)++-- | Build the union of a collection of clauses.+clauseUnion :: Foldable f => f Clause -> Clause+clauseUnion = getClauseUnion . mconcat . fmap ClauseUnion . Foldable.toList++-- | A multi-conjunction.+-- ('//\\') has the following properties.+--+-- __Associativity__+--+-- prop> (f //\\ g) //\\ h == f //\\ (g //\\ h)+--+-- __Left identity__+--+-- prop> [] //\\ g == g+--+-- __Right identity__+--+-- prop> f //\\ [] == f+--+-- __Left zero__+--+-- prop> [Falsity] //\\ g == [Falsity]+--+-- __Right zero__+--+-- prop> f //\\ [Falsity] == [Falsity]+--+(//\\) :: [Formula] -> [Formula] -> [Formula]+[Falsity] //\\ _ = [Falsity]+_ //\\ [Falsity] = [Falsity]+fs //\\ gs = fs <> gs++-- | The ('[]', '//\\') monoid with the absorbing element '[Falsity]'.+newtype MultiConjunction = MultiConjunction { getMultiConjunction :: [Formula] }+ deriving (Show, Eq, Ord)++multiConjunction :: Formula -> MultiConjunction+multiConjunction = \case+ Tautology -> MultiConjunction []+ f -> MultiConjunction [f]++instance Semigroup MultiConjunction where+ (<>) = coerce (//\\)++instance Monoid MultiConjunction where+ mempty = multiConjunction Tautology+ mappend = (<>)++-- | Remove redundant boolean constants from a list of conjuncted formulas.+--+-- >>> flattenConjunction []+-- []+--+-- >>> flattenConjunction [Tautology]+-- []+--+-- >>> flattenConjunction [Falsity]+-- [Atomic (Propositional False)]+--+-- >>> flattenConjunction ["p", Tautology]+-- [Atomic (Predicate (PredicateSymbol "p") [])]+--+-- >>> flattenConjunction ["p", Falsity, "q"]+-- [Atomic (Propositional False)]+--+flattenConjunction :: Foldable f => f Formula -> [Formula]+flattenConjunction = getMultiConjunction . mconcat . fmap multiConjunction . Foldable.toList++-- | A multi-disjunction.+-- ('\\//') has the following properties.+--+-- __Associativity__+--+-- prop> (f \\// g) \\// h == f \\// (g \\// h)+--+-- __Left identity__+--+-- prop> [] \\// g == g+--+-- __Right identity__+--+-- prop> f \\// [] == f+--+-- __Left zero__+--+-- prop> [Tautology] \\// g == [Tautology]+--+-- __Right zero__+--+-- prop> f \\// [Tautology] == [Tautology]+--+(\\//) :: [Formula] -> [Formula] -> [Formula]+[Tautology] \\// _ = [Tautology]+_ \\// [Tautology] = [Tautology]+fs \\// gs = fs <> gs++-- | The ('[]', '\\//') monoid with the absorbing element '[Tautology]'.+newtype MultiDisjunction = MultiDisjunction { getMultiDisjunction :: [Formula] }+ deriving (Show, Eq, Ord)++multiDisjunction :: Formula -> MultiDisjunction+multiDisjunction = \case+ Falsity -> MultiDisjunction []+ f -> MultiDisjunction [f]++instance Semigroup MultiDisjunction where+ (<>) = coerce (\\//)++instance Monoid MultiDisjunction where+ mempty = multiDisjunction Falsity+ mappend = (<>)++-- | Remove redundant boolean constants from a list of disjuncted formulas.+--+-- >>> flattenDisjunction []+-- []+--+-- >>> flattenDisjunction [Tautology]+-- [Atomic (Propositional True)]+--+-- >>> flattenDisjunction [Falsity]+-- []+--+-- >>> flattenDisjunction ["p", Tautology, "q"]+-- [Atomic (Propositional True)]+--+-- >>> flattenDisjunction ["p", Falsity]+-- [Atomic (Predicate (PredicateSymbol "p") [])]+--+flattenDisjunction :: Foldable f => f Formula -> [Formula]+flattenDisjunction = getMultiDisjunction . mconcat . fmap multiDisjunction . Foldable.toList
+ src/ATP/Internal/Enumeration.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++{-|+Module : ATP.Internal.Enumeration+Description : The helper Enumeration monad used to describe computations that+ carry on a renaming of values to consecutive numbers.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module ATP.Internal.Enumeration (+ EnumerationT(..),+ evalEnumerationT,+ Enumeration,+ evalEnumeration,+ next,+ enumerate,+ alias+) where++import Control.Monad.State (MonadTrans, MonadState, StateT, evalStateT, gets, modify)+import Data.Functor.Identity (Identity(..))+import Data.Map (Map)+import qualified Data.Map as M (empty, lookup, insert)+++newtype EnumerationT a m s = EnumerationT {+ runEnumerationT :: StateT (Integer, Map a Integer) m s+} deriving (Functor, Applicative, Monad, MonadTrans, MonadState (Integer, Map a Integer))++evalEnumerationT :: Monad m => EnumerationT a m e -> m e+evalEnumerationT e = evalStateT (runEnumerationT e) (1, M.empty)++type Enumeration a = EnumerationT a Identity++evalEnumeration :: Enumeration a e -> e+evalEnumeration = runIdentity . evalEnumerationT++next :: Monad m => EnumerationT a m Integer+next = do+ i <- gets fst+ modify $ \(j, m) -> (j + 1, m)+ return i++enumerate :: (Ord a, Monad m) => a -> EnumerationT a m Integer+enumerate v = gets (M.lookup v . snd) >>= \case+ Just w -> return w+ Nothing -> do+ i <- next+ modify $ fmap (M.insert v i)+ return i++alias :: (Ord a, Monad m) => a -> a -> EnumerationT a m ()+alias a b = gets (\(_, m) -> (M.lookup a m, M.lookup b m)) >>= \case+ (Just i, Nothing) -> modify $ fmap (M.insert b i)+ (Nothing, Just i) -> modify $ fmap (M.insert a i)+ (_, _) -> do+ i <- next+ modify $ fmap (M.insert a i)+ modify $ fmap (M.insert b i)
+ src/ATP/Pretty/FOL.hs view
@@ -0,0 +1,283 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE FlexibleInstances #-}++{-|+Module : ATP.Pretty.FOL+Description : Pretty-printers for formulas, theorems and proofs.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental++Pretty-printers for formulas, theorems and proofs.+-}++module ATP.Pretty.FOL (+ Pretty(..),+ pprint,+ hprint+) where++import Control.Applicative (liftA2)+import Control.Monad (foldM)+import Data.Char (digitToInt)+import Data.Foldable (toList)+import Data.Functor (($>))+import Data.List (genericIndex, find)+import Data.List.NonEmpty (NonEmpty(..), nonEmpty)+import Data.Map (Map, (!))+import qualified Data.Text as T (unpack, null)+import System.IO (Handle)++import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))++import ATP.Internal.Enumeration++import ATP.Error+import ATP.FOL+++-- * Helper functions++-- | Pretty print to the standard output.+pprint :: Pretty a => a -> IO ()+pprint = putDoc . pretty++-- | Pretty print to an IO handle.+hprint :: Pretty a => Handle -> a -> IO ()+hprint h = hPutDoc h . pretty++prettySequent :: Pretty a => Doc -> a -> Doc+prettySequent h f = bold (h <> dot) <+> pretty f <> line++prettySequents :: Pretty a => Doc -> [a] -> Doc+prettySequents h = hcat . zipWith sequent [1..]+ where sequent i = prettySequent (h <+> integer i)+++-- * Pretty printer for formulas++prettyVar :: Var -> Doc+prettyVar v = cyan . text $ genericIndex variables (abs v)+ where+ variables :: [String]+ variables = liftA2 prime [0..] ["v", "x", "y", "z", "t"]++ prime :: Integer -> String -> String+ prime n w = letter ++ index+ where+ letter = if v >= 0 then w else w ++ "′"+ index = if n == 0 then "" else fmap ("₀₁₂₃₄₅₆₇₈₉" !!) (digits n)+ digits = fmap digitToInt . show++sepBy :: Doc -> NonEmpty Doc -> Doc+sepBy s = foldl1 (\a b -> a <+> s <+> b)++commaSep :: NonEmpty Doc -> Doc+commaSep (d :| ds) = align $ d <> mconcat (fmap (comma <+>) ds)++prettyApplication :: Doc -> [Doc] -> Doc+prettyApplication s as+ | Just as' <- nonEmpty as = s <> parens (commaSep as')+ | otherwise = s++prettyParens :: Pretty e => (e -> Bool) -> e -> Doc+prettyParens simple e+ | simple e = pretty e+ | otherwise = parens (pretty e)++instance Pretty FunctionSymbol where+ pretty (FunctionSymbol s) = text (T.unpack s)++instance Pretty Term where+ pretty = \case+ Variable v -> prettyVar v+ Function f ts -> prettyApplication (pretty f) (fmap pretty ts)++instance Pretty PredicateSymbol where+ pretty (PredicateSymbol p) = text (T.unpack p)++instance Pretty Literal where+ pretty = \case+ Propositional True -> blue "⟙"+ Propositional False -> blue "⟘"+ Predicate p ts -> prettyApplication (pretty p) (fmap pretty ts)+ Equality a b -> pretty a <+> "=" <+> pretty b++instance Pretty (Signed Literal) where+ pretty = \case+ Signed Negative (Equality a b) -> pretty a <+> "!=" <+> pretty b+ Signed Negative l -> blue "￢" <> pretty l+ Signed Positive l -> pretty l++instance Pretty Clause where+ pretty (Literals ls) = case nonEmpty ls of+ Nothing -> pretty (Propositional False)+ Just nls -> sepBy (pretty Or) (fmap pretty nls)++ prettyList = prettySequents "Axiom"++instance Pretty Connective where+ pretty = blue . \case+ And -> "⋀"+ Or -> "⋁"+ Implies -> "=>"+ Equivalent -> "<=>"+ Xor -> "<~>"++instance Pretty Quantifier where+ pretty = \case+ Forall -> "∀"+ Exists -> "∃"++instance Pretty Formula where+ pretty = \case+ Atomic l -> pretty l+ Negate (Atomic (Equality a b)) -> pretty a <+> "!=" <+> pretty b+ Negate f -> blue "￢" <> prettyParens unitary f+ Connected c f g -> prettyParens (under c) f <+> pretty c+ <+> prettyParens (under c) g+ Quantified q v f -> pretty q <+> prettyVar v <+> dot+ <+> prettyParens unitary f++ prettyList = prettySequents "Axiom"++unitary :: Formula -> Bool+unitary = \case+ Atomic{} -> True+ Negate{} -> True+ Connected{} -> False+ Quantified{} -> True++under :: Connective -> Formula -> Bool+under c = \case+ Connected c' _ _ | c == c' && chainable c -> True+ Quantified{} -> False+ f -> unitary f++chainable :: Connective -> Bool+chainable = \case+ And -> True+ Or -> True+ Implies -> False+ Equivalent -> False+ Xor -> False++instance Pretty LogicalExpression where+ pretty = \case+ Clause c -> pretty c+ Formula f -> pretty f+++-- * Pretty printer for problems++instance Pretty Clauses where+ pretty (Clauses cs) = prettyList cs++instance Pretty Theorem where+ pretty (Theorem as c) = prettyList as <> prettySequent "Conjecture" c+++-- * Pretty printer for proofs++instance Pretty l => Pretty (Rule l) where+ pretty rule = pretty (ruleName rule) <> case nonEmpty (toList rule) of+ Just as -> space <> commaSep (fmap (bold . pretty) as)+ Nothing -> empty++instance Pretty RuleName where+ pretty (RuleName rn) =+ case rn of+ "negated conjecture" -> underline (yellow name)+ "unknown" -> red name+ "other" -> name+ _ -> yellow name+ where+ name = text (T.unpack rn)++instance Pretty l => Pretty (Inference l) where+ pretty (Inference r f) = pretty f <+> brackets (pretty r)++instance Pretty l => Pretty (Sequent l) where+ pretty (Sequent c i) = bold (pretty c <> dot) <+> pretty i++instance (Ord l, Pretty l) => Pretty (Derivation l) where+ pretty d = vsep (pretty <$> derivation d) <> line++instance (Ord l, Pretty l) => Pretty (Refutation l) where+ pretty r = vsep (pretty <$> sequents r) <> line++-- | List all sequents that lead to the refutation, sorted topologically+-- breadth-first on the graph of inferences.+sequents :: Ord l => Refutation l -> [Sequent Integer]+sequents (Refutation d c) = evalEnumeration $ do+ ss <- derivationS d+ s <- Sequent <$> next <*> traverse enumerate (liftContradiction c)+ return (reverse (s:ss))++derivation :: Ord l => Derivation l -> [Sequent Integer]+derivation = evalEnumeration . fmap reverse . derivationS++derivationS :: Ord l => Derivation l -> Enumeration l [Sequent Integer]+derivationS d = foldM (sequentsS es) [] ss+ where+ ss = breadthFirst d+ es = labeling ss++sequentsS :: Ord l => Map l LogicalExpression ->+ [Sequent Integer] -> Sequent l ->+ Enumeration l [Sequent Integer]+sequentsS es ss s@(Sequent l i) =+ case find trivialClausification (antecedents i) of+ Just a -> alias l a $> ss+ Nothing -> fmap (:ss) (traverse enumerate s)+ where trivialClausification a = es ! a ~~= consequent i++(~~=) :: LogicalExpression -> LogicalExpression -> Bool+Clause c ~~= Formula f = triviallyClausified f c+Formula f ~~= Clause c = triviallyClausified f c+_ ~~= _ = False++triviallyClausified :: Formula -> Clause -> Bool+triviallyClausified f c+ | Just k <- unliftClause f = k ~= c+ | otherwise = False++instance Pretty Solution where+ pretty = \case+ Saturation d -> vsep [yellow saturated, pretty d]+ Proof r -> vsep [green proven, pretty r]+ where+ saturated = "Disproven by constructing the saturated set of clauses."+ proven = "Found a proof by refutation."++instance Pretty Error where+ pretty err = red $ case explanation of+ Just ex -> vsep [failure, ex]+ Nothing -> failure+ where+ failure = "Failed to find a solution because" <+> reason <> "."++ reason = case err of+ TimeLimitError -> "the theorem prover exceeded its time limit"+ MemoryLimitError -> "the theorem prover exceeded its memory limit"+ ParsingError{} -> "of the following parsing error"+ ProofError{} -> "of the following problem with the proof"+ OtherError{} -> "of the following error"+ ExitCodeError c _ -> "the theorem prover terminated with exit code" <+>+ bold exitCode <+> "and the following error message"+ where exitCode = text (show c)++ explanation = fmap (text . T.unpack) $ case err of+ TimeLimitError -> Nothing+ MemoryLimitError -> Nothing+ ParsingError e -> Just e+ ProofError e -> Just e+ OtherError e -> Just e+ ExitCodeError _ e -> if T.null e then Nothing else Just e++instance Pretty a => Pretty (Partial a) where+ pretty = either pretty pretty . liftPartial
+ src/ATP/Prove.hs view
@@ -0,0 +1,119 @@+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE OverloadedStrings #-}++{-|+Module : ATP.Prove+Description : Interface to automated theorem provers.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental++Interface to automated theorem provers.+-}++module ATP.Prove (+ ProvingOptions(..),+ defaultOptions,+ refute,+ refuteUsing,+ refuteWith,+ prove,+ proveUsing,+ proveWith+) where++import Control.Monad (when)+import Data.Text (Text)+import qualified Data.Text as T (pack)+import Data.TPTP (TPTP)+import Data.TPTP.Parse.Text (parseTSTPOnly)+import Data.TPTP.Pretty (pretty)+import System.Exit (ExitCode(..))+import System.Process (readProcessWithExitCode)+import Text.PrettyPrint.ANSI.Leijen (bold, text)++import ATP.Error+import ATP.FOL (Clauses, Theorem, Solution)+import ATP.Codec.TPTP (encodeClauses, encodeTheorem, decodeSolution)+import ATP.Prover+++-- | The options that describe what theorem prover to use for a problem and+-- how to run it.+data ProvingOptions = ProvingOptions {+ prover :: Prover,+ timeLimit :: TimeLimit,+ memoryLimit :: MemoryLimit,+ debug :: Bool -- ^ If @True@, print the input, the cli command,+ -- the exit code and the output of the prover+} deriving (Eq, Show, Ord)++-- | The default options used by 'refute' and 'prove'.+--+-- >>> defaultOptions+-- ProvingOptions {prover = Prover {vendor = E, executable = "eprover"}, timeLimit = 300, memoryLimit = 2000, debug = False}+defaultOptions :: ProvingOptions+defaultOptions = ProvingOptions {+ prover = defaultProver,+ timeLimit = 300,+ memoryLimit = 2000,+ debug = False+}++-- | Attempt to refute a set of clauses using 'defaultProver'.+--+-- > refute = refuteWith defaultOptions+refute :: Clauses -> IO (Partial Solution)+refute = refuteWith defaultOptions++-- | Attempt to refute a set of clauses using a given prover.+refuteUsing :: Prover -> Clauses -> IO (Partial Solution)+refuteUsing p = refuteWith defaultOptions{prover = p}++-- | Attempt to refute a set of clauses with a given set of options.+refuteWith :: ProvingOptions -> Clauses -> IO (Partial Solution)+refuteWith opts = runWith opts . encodeClauses++-- | Attempt to prove a theorem using 'defaultProver'.+--+-- > prove = proveWith defaultOptions+prove :: Theorem -> IO (Partial Solution)+prove = proveWith defaultOptions++-- | Attempt to prove a theorem using a given prover.+proveUsing :: Prover -> Theorem -> IO (Partial Solution)+proveUsing p = proveWith defaultOptions{prover = p}++-- | Attempt to prove a theorem with a given set of options.+proveWith :: ProvingOptions -> Theorem -> IO (Partial Solution)+proveWith opts = runWith opts . encodeTheorem++runWith :: ProvingOptions -> TPTP -> IO (Partial Solution)+runWith opts tptp = do+ let ProvingOptions{prover} = opts+ let Prover{vendor} = prover+ let input = show (pretty tptp)+ (exitCode, stdout, stderr) <- runProver opts input+ let output = proverOutput vendor exitCode stdout stderr+ let solution = output >>= parseSolution+ return solution++runProver :: ProvingOptions -> String -> IO (ExitCode, Text, Text)+runProver opts input = do+ let ProvingOptions{prover, timeLimit, memoryLimit, debug} = opts+ let Prover{vendor, executable} = prover+ let arguments = proverArguments vendor timeLimit memoryLimit+ let debugPrint header str = when debug $+ print (bold (text header)) >>+ putStrLn str >> putStr "\n"+ debugPrint "Input" input+ debugPrint "Command" $ unwords (executable:arguments)+ (exitCode, stdout, stderr) <- readProcessWithExitCode executable arguments input+ debugPrint "Exit code" (show exitCode)+ debugPrint "Standard output" stdout+ debugPrint "Standard error" stderr+ return (exitCode, T.pack stdout, T.pack stderr)++parseSolution :: Text -> Partial Solution+parseSolution = either parsingError decodeSolution . parseTSTPOnly
+ src/ATP/Prover.hs view
@@ -0,0 +1,102 @@+{-# LANGUAGE OverloadedStrings #-}++{-|+Module : ATP.Prover+Description : Models of automated theorem provers.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental++Models of automated theorem provers.+-}++module ATP.Prover (+ Vendor(..),+ Prover(..),+ TimeLimit,+ MemoryLimit,+ proverArguments,+ proverOutput,+ vampire,+ eprover,+ defaultProver+) where++import Data.Text (Text)+import qualified Data.Text as T (isInfixOf)+import System.Exit (ExitCode(..))++import ATP.Error+++-- | The automated theorem prover.+data Prover = Prover {+ vendor :: Vendor,+ executable :: FilePath+} deriving (Eq, Show, Ord)++-- | The implementation of a theorem prover, supported by @atp@.+data Vendor+ = E+ | Vampire+ deriving (Eq, Show, Ord, Enum, Bounded)++-- | The time limit allocated to the prover, in seconds.+type TimeLimit = Int++-- | The memory limit allocated to the prover, in Mb.+type MemoryLimit = Int++-- | Build the list of command line arguments for the given prover.+proverArguments :: Vendor -> TimeLimit -> MemoryLimit -> [String]+proverArguments E timeLimit memoryLimit =+ ["--proof-object",+ "--silent",+ "--soft-cpu-limit=" ++ show timeLimit,+ "--memory-limit=" ++ show memoryLimit]+proverArguments Vampire timeLimit memoryLimit =+ ["--proof", "tptp",+ "--statistics", "none",+ "--time_limit", show timeLimit,+ "--memory_limit", show memoryLimit]++-- | Interpret the output of the theorem prover from its exit code and+-- the contents of the returned stdout and stderr.+proverOutput :: Vendor+ -> ExitCode+ -> Text -- ^ Standard out+ -> Text -- ^ Standard error+ -> Partial Text+proverOutput E exitCode stdout stderr = case exitCode of+ ExitSuccess -> return stdout+ ExitFailure 1 -> return stdout+ ExitFailure 8 -> timeLimitError+ ExitFailure c -> exitCodeError c stderr+proverOutput Vampire exitCode stdout stderr = case exitCode of+ ExitSuccess -> return stdout+ ExitFailure 1+ | "Time limit reached" `T.isInfixOf` stdout -> timeLimitError+ | "Memory limit exceeded" `T.isInfixOf` stdout -> memoryLimitError+ ExitFailure c -> exitCodeError c stderr++-- | The <http://www.eprover.org/ E> theorem prover.+eprover :: Prover+eprover = Prover {+ vendor = E,+ executable = "eprover"+}++-- | The <https://vprover.github.io/ Vampire> theorem prover.+vampire :: Prover+vampire = Prover {+ vendor = Vampire,+ executable = "vampire"+}++-- | The default prover used by @refute@ and @prove@.+--+-- >>> defaultProver+-- Prover {vendor = E, executable = "eprover"}+defaultProver :: Prover+defaultProver = eprover
+ test/Doc/Main.hs view
@@ -0,0 +1,19 @@+{-|+Module : Doc.Main+Description : Runner of doctests.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module Main where++import Test.DocTest (doctest)++main :: IO ()+main = doctest ["-isrc", "-itest", "--fast",+ "src/ATP/FirstOrder/Formula.hs",+ "src/ATP/FirstOrder/Occurrence.hs",+ "src/ATP/FirstOrder/Conversion.hs",+ "src/ATP/Codec/TPTP.hs"]
+ test/Property/Generators.hs view
@@ -0,0 +1,122 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE CPP #-}++{-|+Module : Property.Generators+Description : QuickCheck generators of first-order formulas, theorems and proofs.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module Property.Generators () where++import GHC.Generics (Generic)+import Generic.Random (genericArbitraryU, genericArbitraryRec, (%), uniform)++import Data.Text (pack)+import Test.QuickCheck (Arbitrary(..), listOf1, choose, genericShrink)++import ATP.FOL+++-- * Formulas++deriving instance Generic FunctionSymbol+instance Arbitrary FunctionSymbol where+ arbitrary = FunctionSymbol . pack <$> listOf1 (choose ('a', 'z'))++deriving instance Generic Term+instance Arbitrary Term where+ arbitrary = genericArbitraryRec uniform+ shrink = genericShrink++deriving instance Generic PredicateSymbol+instance Arbitrary PredicateSymbol where+ arbitrary = PredicateSymbol . pack <$> listOf1 (choose ('A', 'Z'))++deriving instance Generic Literal+instance Arbitrary Literal where+ arbitrary = genericArbitraryRec (1 % 2 % 2 % ())+ shrink = genericShrink++deriving instance Generic Sign+instance Arbitrary Sign where+ arbitrary = genericArbitraryU++deriving instance Generic (Signed a)+instance Arbitrary a => Arbitrary (Signed a) where+ arbitrary = genericArbitraryU+ shrink = genericShrink++deriving instance Generic Clause+instance Arbitrary Clause where+ arbitrary = genericArbitraryU+ shrink = genericShrink++deriving instance Generic Quantifier+instance Arbitrary Quantifier where+ arbitrary = genericArbitraryU++deriving instance Generic Connective+instance Arbitrary Connective where+ arbitrary = genericArbitraryU++deriving instance Generic Formula+instance Arbitrary Formula where+ arbitrary = genericArbitraryRec (3 % 2 % 1 % 2 % ())+ shrink = genericShrink++deriving instance Generic LogicalExpression+instance Arbitrary LogicalExpression where+ arbitrary = genericArbitraryU+ shrink = genericShrink+++-- * Problems++deriving instance Generic Clauses+instance Arbitrary Clauses where+ arbitrary = genericArbitraryU+ shrink = genericShrink++deriving instance Generic Theorem+instance Arbitrary Theorem where+ arbitrary = genericArbitraryU+ shrink = genericShrink+++-- * Proofs++instance Arbitrary RuleName where+ arbitrary = RuleName . pack <$> listOf1 (choose ('a', 'z'))++deriving instance Generic (Rule f)+instance Arbitrary f => Arbitrary (Rule f) where+ arbitrary = genericArbitraryU++deriving instance Generic (Inference f)+instance Arbitrary f => Arbitrary (Inference f) where+ arbitrary = genericArbitraryU++deriving instance Generic (Contradiction f)+instance Arbitrary f => Arbitrary (Contradiction f) where+ arbitrary = genericArbitraryU++deriving instance Generic (Sequent f)+instance Arbitrary f => Arbitrary (Sequent f) where+ arbitrary = genericArbitraryU++deriving instance Generic (Derivation f)+instance (Ord f, Arbitrary f) => Arbitrary (Derivation f) where+ arbitrary = genericArbitraryU+ shrink = genericShrink++deriving instance Generic (Refutation f)+instance (Ord f, Arbitrary f) => Arbitrary (Refutation f) where+ arbitrary = genericArbitraryU+ shrink = genericShrink
+ test/Property/Main.hs view
@@ -0,0 +1,319 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE TemplateHaskell #-}++{-|+Module : Main+Description : QuickCheck properties of the atp library.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module Main (main) where++import Control.Monad (unless)+import Data.Function (on)+#if !MIN_VERSION_base(4, 11, 0)+import Data.Semigroup (Semigroup(..))+#endif+import System.Exit (exitFailure)++import Test.QuickCheck (+ Testable, Property, property, (===), (==>), counterexample, forAll,+ forAllProperties, quickCheckWithResult, stdArgs, Args(..), withMaxSuccess+ )++import ATP hiding ((===), (==>))+import ATP.Codec.TPTP++import Property.Generators ()+import Property.Modifiers.AlphaEquivalent+++-- * Helper functions++infix 4 ~==+infix 4 ~~=+infix 4 ~==~++-- | Like '(===)', but for alpha equivalence.+(~==) :: (Show e, FirstOrder e) => e -> e -> Property+a ~== b = counterexample (show a ++ " ~/= " ++ show b) (a ~= b)++-- | Like '(~==)', but for results of partial computations.+(~~=) :: (Show e, FirstOrder e) => Partial e -> Partial e -> Property+x ~~= y+ | Right a <- liftPartial x, Right b <- liftPartial y = a ~== b+ | otherwise = counterexample (show x ++ " ~/= " ++ show y) False++-- | Like '(~==~)', but modulo simplification.+(~==~) :: (Show e, FirstOrder e, Simplify e) => Partial e -> Partial e -> Property+(~==~) = (~~=) `on` fmap simplify++satisfies :: (Show b, Testable prop) => (a -> b) -> (b -> prop) -> a -> Property+satisfies f p a = counterexample (show b) (p b) where b = f a+++-- * Generators++-- ** 'genAlphaEquivalent' does not introduce new free variables++freeCountAlphaEquivalent :: (Show e, FirstOrder e) => e -> Property+freeCountAlphaEquivalent a =+ forAll (genAlphaEquivalent a) $ \b ->+ length (free a) === length (free b)++prop_freeCountAlphaEquivalentFormula :: Formula -> Property+prop_freeCountAlphaEquivalentFormula =+ withMaxSuccess 100000 . freeCountAlphaEquivalent++prop_freeCountAlphaEquivalentClause :: Clause -> Property+prop_freeCountAlphaEquivalentClause = freeCountAlphaEquivalent++prop_freeCountAlphaEquivalentLiteral :: Literal -> Property+prop_freeCountAlphaEquivalentLiteral = freeCountAlphaEquivalent++prop_freeCountAlphaEquivalentTerm :: Term -> Property+prop_freeCountAlphaEquivalentTerm = freeCountAlphaEquivalent+++-- ** 'genAlphaEquivalent' produces alpha equivalent expressions++actuallyAlphaEquivalent :: (Show e, FirstOrder e) => e -> Property+actuallyAlphaEquivalent a =+ forAll (genAlphaEquivalent a) $ \b ->+ a ~= b++prop_actuallyAlphaEquivalentFormula :: Formula -> Property+prop_actuallyAlphaEquivalentFormula =+ withMaxSuccess 100000 . actuallyAlphaEquivalent++prop_actuallyAlphaEquivalentClause :: Clause -> Property+prop_actuallyAlphaEquivalentClause = actuallyAlphaEquivalent++prop_actuallyAlphaEquivalentLiteral :: Literal -> Property+prop_actuallyAlphaEquivalentLiteral = actuallyAlphaEquivalent++prop_actuallyAlphaEquivalentTerm :: Term -> Property+prop_actuallyAlphaEquivalentTerm = actuallyAlphaEquivalent+++-- ** 'genAlphaInequivalent' produces alpha inequivalent expressions++actuallyAlphaInequivalent :: (Show e, FirstOrder e) => e -> Property+actuallyAlphaInequivalent a =+ length (vars a) > 1 ==>+ forAll (genAlphaInequivalent a) $ \b ->+ not (a ~= b)++prop_actuallyAlphaInequivalentFormula :: Formula -> Property+prop_actuallyAlphaInequivalentFormula =+ withMaxSuccess 50000 . actuallyAlphaInequivalent++prop_actuallyAlphaInequivalentClause :: Clause -> Property+prop_actuallyAlphaInequivalentClause = actuallyAlphaInequivalent++prop_actuallyAlphaInequivalentLiteral :: Literal -> Property+prop_actuallyAlphaInequivalentLiteral = actuallyAlphaInequivalent++prop_actuallyAlphaInequivalentTerm :: Term -> Property+prop_actuallyAlphaInequivalentTerm = actuallyAlphaInequivalent+++-- * Free and bound variables++freeBoundVars :: FirstOrder e => e -> Property+freeBoundVars e = free e <> bound e === vars e++prop_freeBoundVarsFormula :: Formula -> Property+prop_freeBoundVarsFormula = freeBoundVars++prop_freeBoundVarsClause :: Clause -> Property+prop_freeBoundVarsClause = freeBoundVars++prop_freeBoundVarsLiteral :: Literal -> Property+prop_freeBoundVarsLiteral = freeBoundVars++prop_freeBoundVarsTerm :: Term -> Property+prop_freeBoundVarsTerm = freeBoundVars+++-- * Alpha equivalence++-- ** Alpha equivalence is reflexive++alphaEquivalenceReflexivity :: FirstOrder e => e -> Property+alphaEquivalenceReflexivity e = property (e ~= e)++prop_alphaEquivalenceReflexivityFormula :: Formula -> Property+prop_alphaEquivalenceReflexivityFormula =+ withMaxSuccess 100000 . alphaEquivalenceReflexivity++prop_alphaEquivalenceReflexivityClause :: Clause -> Property+prop_alphaEquivalenceReflexivityClause = alphaEquivalenceReflexivity++prop_alphaEquivalenceReflexivityLiteral :: Literal -> Property+prop_alphaEquivalenceReflexivityLiteral = alphaEquivalenceReflexivity++prop_alphaEquivalenceReflexivityTerm :: Term -> Property+prop_alphaEquivalenceReflexivityTerm = alphaEquivalenceReflexivity+++-- ** Alpha equivalence is symmetric++alphaEquivalenceSymmetry :: (Show e, FirstOrder e) => e -> Property+alphaEquivalenceSymmetry a =+ forAll (genAlphaEquivalent a) $ \b ->+ b ~= a++prop_alphaEquivalenceSymmetryFormula :: Formula -> Property+prop_alphaEquivalenceSymmetryFormula =+ withMaxSuccess 100000 . alphaEquivalenceSymmetry++prop_alphaEquivalenceSymmetryClause :: Clause -> Property+prop_alphaEquivalenceSymmetryClause = alphaEquivalenceSymmetry++prop_alphaEquivalenceSymmetryLiteral :: Literal -> Property+prop_alphaEquivalenceSymmetryLiteral = alphaEquivalenceSymmetry++prop_alphaEquivalenceSymmetryTerm :: Term -> Property+prop_alphaEquivalenceSymmetryTerm = alphaEquivalenceSymmetry+++-- ** Alpha equivalence is transitive++alphaEquivalenceTransitivity :: (Show e, FirstOrder e) => e -> Property+alphaEquivalenceTransitivity a =+ forAll (genAlphaEquivalent a) $ \b ->+ forAll (genAlphaEquivalent b) $ \c ->+ a ~= c++prop_alphaEquivalenceTransitivityFormula :: Formula -> Property+prop_alphaEquivalenceTransitivityFormula =+ withMaxSuccess 100000 . alphaEquivalenceTransitivity++prop_alphaEquivalenceTransitivityClause :: Clause -> Property+prop_alphaEquivalenceTransitivityClause = alphaEquivalenceTransitivity++prop_alphaEquivalenceTransitivityLiteral :: Literal -> Property+prop_alphaEquivalenceTransitivityLiteral = alphaEquivalenceTransitivity++prop_alphaEquivalenceTransitivityTerm :: Term -> Property+prop_alphaEquivalenceTransitivityTerm = alphaEquivalenceTransitivity+++-- * Simplification++-- ** Clauses++prop_simplifyClause :: Clause -> Property+prop_simplifyClause = simplify `satisfies` isSimplifiedClause++isSimplifiedClause :: Clause -> Bool+isSimplifiedClause (Literals ls) =+ not (any isNegatedConstant ls) &&+ FalsityLiteral `notElem` ls &&+ (ls == [TautologyLiteral] || TautologyLiteral `notElem` ls)++isNegatedConstant :: Signed Literal -> Bool+isNegatedConstant = \case+ Signed Negative Propositional{} -> True+ _ -> False++prop_simplifyClauses :: Clauses -> Property+prop_simplifyClauses = simplify `satisfies` areSimplifiedClauses++areSimplifiedClauses :: Clauses -> Bool+areSimplifiedClauses (Clauses []) = True+areSimplifiedClauses (Clauses cs) =+ all isSimplifiedClause cs &&+ (cs == [EmptyClause] || EmptyClause `notElem` cs)+++-- ** Formulas++prop_simplifyFormula :: Formula -> Property+prop_simplifyFormula = simplify `satisfies` isSimplifiedFormula++isSimplifiedFormula :: Formula -> Bool+isSimplifiedFormula f =+ not (containsDoubleNegation f) &&+ not (containsLeftAssocitivity f)++containsDoubleNegation :: Formula -> Bool+containsDoubleNegation = \case+ Atomic{} -> False+ Negate Negate{} -> True+ Negate f -> containsDoubleNegation f+ Connected _ f g -> containsDoubleNegation f || containsDoubleNegation g+ Quantified _ _ f -> containsDoubleNegation f++containsLeftAssocitivity :: Formula -> Bool+containsLeftAssocitivity = \case+ Atomic{} -> False+ Negate f -> containsLeftAssocitivity f+ Connected c (Connected c' _ _) _ | c' == c && isAssociative c -> True+ Connected _ f g -> containsLeftAssocitivity f || containsLeftAssocitivity g+ Quantified _ _ f -> containsLeftAssocitivity f+++-- ** Idempotence++simplifyIdempotent :: (Eq a, Show a, Simplify a) => a -> Property+simplifyIdempotent a = simplify a ==~ a+ where (==~) = (===) `on` simplify++prop_simplifyIdempotentClause :: Clause -> Property+prop_simplifyIdempotentClause = simplifyIdempotent++prop_simplifyIdempotentFormula :: Formula -> Property+prop_simplifyIdempotentFormula = simplifyIdempotent++prop_simplifyIdempotentLogicalExpression :: LogicalExpression -> Property+prop_simplifyIdempotentLogicalExpression = simplifyIdempotent++prop_simplifyIdempotentClauses :: Clauses -> Property+prop_simplifyIdempotentClauses = simplifyIdempotent++prop_simplifyIdempotentTheorem :: Theorem -> Property+prop_simplifyIdempotentTheorem = simplifyIdempotent+++-- * Conversions++prop_liftUnliftSignedLiteral :: Signed Literal -> Property+prop_liftUnliftSignedLiteral s =+ unliftSignedLiteral (liftSignedLiteral s) === Just s++prop_liftUnliftClause :: Clause -> Property+prop_liftUnliftClause c = unliftClause (liftClause c) ==~ Just c+ where (==~) = (===) `on` fmap simplify++prop_liftUnliftContradiction :: (Show f, Eq f) => Contradiction f -> Property+prop_liftUnliftContradiction c =+ unliftContradiction (liftContradiction c) === Just c+++-- * Codec++prop_codecClause :: Clause -> Property+prop_codecClause c = return c ~==~ decodeClause (encodeClause c)++prop_codecFormula :: Formula -> Property+prop_codecFormula f = return f ~==~ decodeFormula (encodeFormula f)++prop_codec :: LogicalExpression -> Property+prop_codec e = return e ~==~ decode (encode e)+++-- * Runner++return []++main :: IO ()+main = do+ let args = stdArgs{maxSuccess=1000, maxDiscardRatio=50}+ success <- $forAllProperties (quickCheckWithResult args)+ unless success exitFailure
+ test/Property/Modifiers/AlphaEquivalent.hs view
@@ -0,0 +1,65 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleInstances #-}++{-|+Module : Property.Modifiers.AlphaEquivalent+Description : QuickCheck generators of alpha-equivalent and alpha-inequivalent+ first-order expressions.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module Property.Modifiers.AlphaEquivalent (+ genAlphaEquivalent,+ genAlphaInequivalent+) where++import Control.Monad.Trans (lift)++import Test.QuickCheck (Arbitrary(..), Gen, suchThat, elements)++import ATP.FOL+++-- * Alpha-equivalent first-order expressions.++genAlphaEquivalent :: FirstOrder e => e -> Gen e+genAlphaEquivalent = getAlphaEquivalence . evalAlphaT . alpha++newtype AlphaEquivalence m a = AlphaEquivalence { getAlphaEquivalence :: m a }+ deriving (Functor, Applicative, Monad)++instance MonadAlpha (AlphaEquivalence Gen) where+ binding _ = fresh+ occurrence = return+++-- * Alpha-inequivalent first-order expressions.++genAlphaInequivalent :: FirstOrder e => e -> Gen e+genAlphaInequivalent = getAlphaInequivalence . evalAlphaT . alpha++newtype AlphaInequivalence m a = AlphaInequivalence { getAlphaInequivalence :: m a }+ deriving (Functor, Applicative, Monad)++instance MonadAlpha (AlphaInequivalence Gen) where+ binding _ = stale+ occurrence = anythingBut+++-- * Helper functions++fresh :: AlphaT (AlphaEquivalence Gen) Var+fresh = do+ vs <- scope+ lift . AlphaEquivalence $ arbitrary `suchThat` (`notElem` vs)++stale :: AlphaT (AlphaInequivalence Gen) Var+stale = do+ vs <- scope+ lift . AlphaInequivalence $ if null vs then arbitrary else elements vs++anythingBut :: Var -> AlphaT (AlphaInequivalence Gen) Var+anythingBut v = lift . AlphaInequivalence $ arbitrary `suchThat` (/= v)
+ test/Property/Modifiers/Simplified.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE DeriveTraversable #-}++{-|+Module : Property.Modifiers.Simplified+Description : QuickCheck generators of simplified first-order expressions.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module Property.Modifiers.Simplified (+ Simplified(..)+) where++import Test.QuickCheck (Arbitrary(..))++import Property.Generators ()++import ATP.FOL+++newtype Simplified a = Simplified { getSimplified :: a }+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++instance (Simplify e, Arbitrary e) => Arbitrary (Simplified e) where+ arbitrary = Simplified . simplify <$> arbitrary+ shrink = traverse (fmap simplify . shrink)
+ test/Unit/Main.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}++{-|+Module : Unit.Main+Description : Basic unit tests.+Copyright : (c) Evgenii Kotelnikov, 2019-2021+License : GPL-3+Maintainer : evgeny.kotelnikov@gmail.com+Stability : experimental+-}++module Unit.Main (tests) where++import Distribution.TestSuite (Test(..), TestInstance(..),+ Progress(..), Result(..))+import ATP+++-- * Helpers++simpleTest :: String -> IO Progress -> Test+simpleTest nm progress = Test $ TestInstance {+ name = nm,+ tags = [],+ options = [],+ setOption = const . const $ Left "not supported",+ run = progress+}++testCase :: Prover -> String ->+ (Either Error Solution -> Result) ->+ Either Clauses Theorem -> Test+testCase p nm testAnswer input = simpleTest testName progress+ where+ testName = show (vendor p) ++ " " ++ nm+ progress = fmap (Finished . testAnswer . liftPartial) solution+ solution = case input of+ Left cs -> refuteWith opts cs+ Right t -> proveWith opts t+ opts = defaultOptions{prover=p, timeLimit=5}++expectSolution :: (Solution -> Result) -> Either Error Solution -> Result+expectSolution testSolution = \case+ Left e -> Error ("Failed to find a solution: " ++ show e)+ Right s -> testSolution s++expectSaturation :: Either Error Solution -> Result+expectSaturation = expectSolution $ \case+ Saturation{} -> Pass+ Proof{} -> Error "Unexpected proof"++expectProof :: Either Error Solution -> Result+expectProof = expectSolution $ \case+ Saturation{} -> Error "Unexpected saturation"+ Proof{} -> Pass++expectTimLimitError :: Either Error Solution -> Result+expectTimLimitError = \case+ Left TimeLimitError -> Pass+ Left e -> Error $ "Unexpected error " ++ show e+ Right _ -> Error "Unexpected solution"+++-- * Test data++emptyClause :: Clauses+emptyClause = Clauses [EmptyClause]++negated :: Theorem -> Theorem+negated (Theorem as c) = Theorem as (neg c)++syllogism :: Theorem+syllogism = [humansAreMortal, human "socrates"] |- mortal "socrates"+ where+ humansAreMortal = forall $ \x -> human x ==> mortal x+ human = UnaryPredicate "human"+ mortal = UnaryPredicate "mortal"++groupTheoryAxiom :: Theorem+groupTheoryAxiom = [leftIdentity, leftInverse, associativity, groupOfOrder2] |- commutativity+ where+ inverse = UnaryFunction "inverse"+ (.*.) = BinaryFunction "mult"+ leftIdentity = forall $ \x -> "e" .*. x === x+ leftInverse = forall $ \x -> inverse x .*. x === "e"+ associativity = forall $ \x y z -> (x .*. y) .*. z === x .*. (y .*. z)+ groupOfOrder2 = forall $ \x -> x .*. x === "e"+ commutativity = forall $ \x y -> x .*. y === y .*. x+++-- * Test suite++tests :: IO [Test]+tests = return [testCase p n t i | (n, t, i) <- cases, p <- provers]+ where+ provers = [eprover, vampire]+ cases = [+ ("refutes an empty clause", expectProof, Left emptyClause),+ ("saturates an empty clause set", expectSaturation, Left (Clauses [])),++ ("proves tautology", expectProof, Right (Claim Tautology)),+ ("saturates falsity", expectSaturation, Right (Claim Falsity)),++ ("proves syllogism", expectProof, Right syllogism),+ ("saturates negated syllogism", expectSaturation, Right (negated syllogism)),++ ("proves group theory axiom", expectProof, Right groupTheoryAxiom),+ ("reached time limit", expectTimLimitError, Right (negated groupTheoryAxiom))+ ]