diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for atp + +## 0.1.0.0 -- 2021-01-25 + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + + Copyright (C) + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + Copyright (C) + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +. + + The GNU General Public License does not permit incorporating your program +into proprietary programs. If your program is a subroutine library, you +may consider it more useful to permit linking proprietary applications with +the library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. But first, please read +. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/atp.cabal b/atp.cabal new file mode 100644 --- /dev/null +++ b/atp.cabal @@ -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 diff --git a/src/ATP.hs b/src/ATP.hs new file mode 100644 --- /dev/null +++ b/src/ATP.hs @@ -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'. diff --git a/src/ATP/Codec/TPTP.hs b/src/ATP/Codec/TPTP.hs new file mode 100644 --- /dev/null +++ b/src/ATP/Codec/TPTP.hs @@ -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 diff --git a/src/ATP/Error.hs b/src/ATP/Error.hs new file mode 100644 --- /dev/null +++ b/src/ATP/Error.hs @@ -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 diff --git a/src/ATP/FOL.hs b/src/ATP/FOL.hs new file mode 100644 --- /dev/null +++ b/src/ATP/FOL.hs @@ -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 diff --git a/src/ATP/FirstOrder/Alpha.hs b/src/ATP/FirstOrder/Alpha.hs new file mode 100644 --- /dev/null +++ b/src/ATP/FirstOrder/Alpha.hs @@ -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 diff --git a/src/ATP/FirstOrder/Conversion.hs b/src/ATP/FirstOrder/Conversion.hs new file mode 100644 --- /dev/null +++ b/src/ATP/FirstOrder/Conversion.hs @@ -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 diff --git a/src/ATP/FirstOrder/Core.hs b/src/ATP/FirstOrder/Core.hs new file mode 100644 --- /dev/null +++ b/src/ATP/FirstOrder/Core.hs @@ -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 diff --git a/src/ATP/FirstOrder/Derivation.hs b/src/ATP/FirstOrder/Derivation.hs new file mode 100644 --- /dev/null +++ b/src/ATP/FirstOrder/Derivation.hs @@ -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) diff --git a/src/ATP/FirstOrder/Occurrence.hs b/src/ATP/FirstOrder/Occurrence.hs new file mode 100644 --- /dev/null +++ b/src/ATP/FirstOrder/Occurrence.hs @@ -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 diff --git a/src/ATP/FirstOrder/Simplification.hs b/src/ATP/FirstOrder/Simplification.hs new file mode 100644 --- /dev/null +++ b/src/ATP/FirstOrder/Simplification.hs @@ -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 diff --git a/src/ATP/FirstOrder/Smart.hs b/src/ATP/FirstOrder/Smart.hs new file mode 100644 --- /dev/null +++ b/src/ATP/FirstOrder/Smart.hs @@ -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 +-- . +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 diff --git a/src/ATP/Internal/Enumeration.hs b/src/ATP/Internal/Enumeration.hs new file mode 100644 --- /dev/null +++ b/src/ATP/Internal/Enumeration.hs @@ -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) diff --git a/src/ATP/Pretty/FOL.hs b/src/ATP/Pretty/FOL.hs new file mode 100644 --- /dev/null +++ b/src/ATP/Pretty/FOL.hs @@ -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 diff --git a/src/ATP/Prove.hs b/src/ATP/Prove.hs new file mode 100644 --- /dev/null +++ b/src/ATP/Prove.hs @@ -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 diff --git a/src/ATP/Prover.hs b/src/ATP/Prover.hs new file mode 100644 --- /dev/null +++ b/src/ATP/Prover.hs @@ -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 theorem prover. +eprover :: Prover +eprover = Prover { + vendor = E, + executable = "eprover" +} + +-- | The 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 diff --git a/test/Doc/Main.hs b/test/Doc/Main.hs new file mode 100644 --- /dev/null +++ b/test/Doc/Main.hs @@ -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"] diff --git a/test/Property/Generators.hs b/test/Property/Generators.hs new file mode 100644 --- /dev/null +++ b/test/Property/Generators.hs @@ -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 diff --git a/test/Property/Main.hs b/test/Property/Main.hs new file mode 100644 --- /dev/null +++ b/test/Property/Main.hs @@ -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 diff --git a/test/Property/Modifiers/AlphaEquivalent.hs b/test/Property/Modifiers/AlphaEquivalent.hs new file mode 100644 --- /dev/null +++ b/test/Property/Modifiers/AlphaEquivalent.hs @@ -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) diff --git a/test/Property/Modifiers/Simplified.hs b/test/Property/Modifiers/Simplified.hs new file mode 100644 --- /dev/null +++ b/test/Property/Modifiers/Simplified.hs @@ -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) diff --git a/test/Unit/Main.hs b/test/Unit/Main.hs new file mode 100644 --- /dev/null +++ b/test/Unit/Main.hs @@ -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)) + ]