diff options
63 files changed, 6611 insertions, 0 deletions
diff --git a/proofsearch/.clang-format b/proofsearch/.clang-format new file mode 100644 index 0000000..64f782a --- /dev/null +++ b/proofsearch/.clang-format @@ -0,0 +1,62 @@ +--- +Language: Cpp +BasedOnStyle: Google + +# Indentation +IndentWidth: 4 +TabWidth: 4 +UseTab: Never +AccessModifierOffset: -2 +NamespaceIndentation: None +IndentCaseLabels: true + +# Line width +ColumnLimit: 100 + +# Braces +BreakBeforeBraces: Attach +AllowShortFunctionsOnASingleLine: Inline +AllowShortIfStatementsOnASingleLine: Never +AllowShortLoopsOnASingleLine: false +AllowShortBlocksOnASingleLine: Empty + +# Includes +SortIncludes: CaseSensitive +IncludeBlocks: Regroup +IncludeCategories: + # Project headers + - Regex: '^"atp/' + Priority: 1 + # System / C++ standard headers + - Regex: '^<' + Priority: 2 + # Catch-all + - Regex: '.*' + Priority: 3 + +# Alignment +AlignAfterOpenBracket: Align +AlignConsecutiveAssignments: false +AlignConsecutiveDeclarations: false +AlignOperands: Align +AlignTrailingComments: true + +# Spacing +SpaceAfterCStyleCast: false +SpaceAfterTemplateKeyword: true +SpaceBeforeAssignmentOperators: true +SpaceBeforeParens: ControlStatements +SpacesInAngles: Never + +# Pointer alignment +PointerAlignment: Left +ReferenceAlignment: Left +DerivePointerAlignment: false + +# Other +ReflowComments: true +FixNamespaceComments: true +CompactNamespaces: false +AllowAllParametersOfDeclarationOnNextLine: true +BinPackArguments: true +BinPackParameters: true diff --git a/proofsearch/.clang-tidy b/proofsearch/.clang-tidy new file mode 100644 index 0000000..412e8a8 --- /dev/null +++ b/proofsearch/.clang-tidy @@ -0,0 +1,76 @@ +--- +# ATP Engine clang-tidy configuration +# +# Enable categories incrementally — start strict on the code we write, +# avoid noise from auto-generated code (ANTLR4). + +Checks: > + -*, + bugprone-*, + -bugprone-easily-swappable-parameters, + clang-analyzer-*, + cppcoreguidelines-*, + -cppcoreguidelines-avoid-const-or-ref-data-members, + -cppcoreguidelines-avoid-magic-numbers, + -cppcoreguidelines-pro-type-reinterpret-cast, + -cppcoreguidelines-pro-bounds-pointer-arithmetic, + -cppcoreguidelines-owning-memory, + misc-*, + -misc-no-recursion, + -misc-non-private-member-variables-in-classes, + modernize-*, + -modernize-use-trailing-return-type, + performance-*, + readability-*, + -readability-magic-numbers, + -readability-identifier-length, + +WarningsAsErrors: '' + +HeaderFilterRegex: 'include/atp/.*\.h$' + +CheckOptions: + - key: readability-identifier-naming.NamespaceCase + value: lower_case + - key: readability-identifier-naming.ClassCase + value: CamelCase + - key: readability-identifier-naming.StructCase + value: CamelCase + - key: readability-identifier-naming.FunctionCase + value: camelBack + - key: readability-identifier-naming.VariableCase + value: lower_case + - key: readability-identifier-naming.MemberCase + value: lower_case + - key: readability-identifier-naming.MemberSuffix + value: '_' + - key: readability-identifier-naming.ConstantCase + value: CamelCase + - key: readability-identifier-naming.ConstantPrefix + value: k + - key: readability-identifier-naming.LocalConstantCase + value: lower_case + - key: readability-identifier-naming.LocalConstantPrefix + value: '' + - key: readability-identifier-naming.LocalConstantSuffix + value: '' + - key: readability-identifier-naming.EnumConstantCase + value: CamelCase + - key: readability-identifier-naming.EnumConstantPrefix + value: k + - key: readability-identifier-naming.ConstexprVariableCase + value: CamelCase + - key: readability-identifier-naming.ConstexprVariablePrefix + value: k + - key: readability-identifier-naming.GlobalConstantCase + value: CamelCase + - key: readability-identifier-naming.GlobalConstantPrefix + value: k + - key: readability-identifier-naming.TemplateParameterCase + value: CamelCase + - key: performance-move-const-arg.CheckTriviallyCopyableMove + value: false + - key: cppcoreguidelines-special-member-functions.AllowSoleDefaultDtor + value: true + - key: readability-function-cognitive-complexity.Threshold + value: 25 diff --git a/proofsearch/.gitignore b/proofsearch/.gitignore new file mode 100644 index 0000000..2a1b7e2 --- /dev/null +++ b/proofsearch/.gitignore @@ -0,0 +1,15 @@ +# Build +build/ +cmake-build-*/ +.cache/ +compile_commands.json + +# IDE +.vscode/ +.idea/ +*.swp +*~ + +# OS +.DS_Store +Thumbs.db diff --git a/proofsearch/CMakeLists.txt b/proofsearch/CMakeLists.txt new file mode 100644 index 0000000..2257766 --- /dev/null +++ b/proofsearch/CMakeLists.txt @@ -0,0 +1,111 @@ +cmake_minimum_required(VERSION 3.20) +project(atp_engine + VERSION 0.1.0 + LANGUAGES CXX +) + +# ─── C++ Standard ──────────────────────────────────────────────────────────── +set(CMAKE_CXX_STANDARD 20) +set(CMAKE_CXX_STANDARD_REQUIRED ON) +set(CMAKE_CXX_EXTENSIONS OFF) + +# Export compile_commands.json for clang-tidy and IDE support +set(CMAKE_EXPORT_COMPILE_COMMANDS ON) + +# ─── Compiler Warnings ────────────────────────── +set(ATP_PROJECT_WARNING_FLAGS + -Wall -Wextra -Wpedantic + -Wshadow -Wnon-virtual-dtor + -Wold-style-cast -Wcast-align -Wunused + -Woverloaded-virtual -Wconversion -Wsign-conversion + -Wnull-dereference -Wdouble-promotion + -Wformat=2 -Wimplicit-fallthrough +) + +# ─── Sanitizers (Debug builds) ─────────────────────────────────────────────── +option(ATP_ENABLE_SANITIZERS "Enable ASan + UBSan in Debug builds" ON) +if(ATP_ENABLE_SANITIZERS AND CMAKE_BUILD_TYPE STREQUAL "Debug") + add_compile_options(-fsanitize=address,undefined -fno-omit-frame-pointer) + add_link_options(-fsanitize=address,undefined) +endif() + +# ─── clang-tidy Integration ───────────────────────────────────────────────── +option(ATP_ENABLE_CLANG_TIDY "Enable clang-tidy static analysis" OFF) +if(ATP_ENABLE_CLANG_TIDY) + find_program(CLANG_TIDY_EXE NAMES clang-tidy) + if(CLANG_TIDY_EXE) + message(STATUS "clang-tidy found: ${CLANG_TIDY_EXE}") + else() + message(WARNING "clang-tidy requested but not found") + endif() +endif() + +# ─── clang-format Custom Target ───────────────────────────────────────────── +find_program(CLANG_FORMAT_EXE NAMES clang-format) +if(CLANG_FORMAT_EXE) + file(GLOB_RECURSE ALL_CXX_SOURCES + ${PROJECT_SOURCE_DIR}/src/*.cc + ${PROJECT_SOURCE_DIR}/include/*.h + ${PROJECT_SOURCE_DIR}/tests/*.cc + ) + add_custom_target(format + COMMAND ${CLANG_FORMAT_EXE} -i ${ALL_CXX_SOURCES} + COMMENT "Running clang-format on all source files" + VERBATIM + ) + add_custom_target(format-check + COMMAND ${CLANG_FORMAT_EXE} --dry-run --Werror ${ALL_CXX_SOURCES} + COMMENT "Checking clang-format compliance" + VERBATIM + ) + message(STATUS "clang-format found: ${CLANG_FORMAT_EXE}") + message(STATUS " Use 'cmake --build . --target format' to auto-format") + message(STATUS " Use 'cmake --build . --target format-check' to check format") +else() + message(WARNING "clang-format not found, format targets disabled") +endif() + +# ─── Source Files ──────────────────────────────────────────────────────────── +set(ATP_SOURCES + src/core/symbol_table.cc + src/core/term_bank.cc + src/core/clause_store.cc + src/normalize/clausifier.cc + src/infer/substitution.cc + src/infer/unification.cc + src/infer/resolution.cc + src/index/discrim_tree.cc + src/simplify/subsumption.cc + src/simplify/tautology.cc + src/search/prover.cc + src/proof/proof_trace.cc + src/rewrite/ordering.cc + src/rewrite/paramodulation.cc + src/strategy/problem_analyzer.cc + src/frontend/tptp_parser.cc +) + +# ─── Core Library ──────────────────────────────────────────────────────────── +add_library(atp_core STATIC ${ATP_SOURCES}) +target_include_directories(atp_core PUBLIC + ${PROJECT_SOURCE_DIR}/include +) +target_compile_options(atp_core PRIVATE ${ATP_PROJECT_WARNING_FLAGS}) +if(ATP_ENABLE_CLANG_TIDY AND CLANG_TIDY_EXE) + set_property(TARGET atp_core PROPERTY CXX_CLANG_TIDY "${CLANG_TIDY_EXE}") +endif() + +# ─── Main Executable ──────────────────────────────────────────────────────── +add_executable(atp src/main.cc) +target_link_libraries(atp PRIVATE atp_core) +target_compile_options(atp PRIVATE ${ATP_PROJECT_WARNING_FLAGS}) +if(ATP_ENABLE_CLANG_TIDY AND CLANG_TIDY_EXE) + set_property(TARGET atp PROPERTY CXX_CLANG_TIDY "${CLANG_TIDY_EXE}") +endif() + +# ─── Tests ─────────────────────────────────────────────────────────────────── +option(ATP_BUILD_TESTS "Build unit tests" ON) +if(ATP_BUILD_TESTS) + enable_testing() + add_subdirectory(tests) +endif() diff --git a/proofsearch/LICENSE b/proofsearch/LICENSE new file mode 100644 index 0000000..f288702 --- /dev/null +++ b/proofsearch/LICENSE @@ -0,0 +1,674 @@ + GNU GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/> + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The GNU General Public License is a free, copyleft license for +software and other kinds of works. + + The licenses for most software and other practical works are designed +to take away your freedom to share and change the works. By contrast, +the GNU General Public License is intended to guarantee your freedom to +share and change all versions of a program--to make sure it remains free +software for all its users. We, the Free Software Foundation, use the +GNU General Public License for most of our software; it applies also to +any other work released this way by its authors. You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +them if you wish), that you receive source code or can get it if you +want it, that you can change the software or use pieces of it in new +free programs, and that you know you can do these things. + + To protect your rights, we need to prevent others from denying you +these rights or asking you to surrender the rights. Therefore, you have +certain responsibilities if you distribute copies of the software, or if +you modify it: responsibilities to respect the freedom of others. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must pass on to the recipients the same +freedoms that you received. You must make sure that they, too, receive +or can get the source code. And you must show them these terms so they +know their rights. + + Developers that use the GNU GPL protect your rights with two steps: +(1) assert copyright on the software, and (2) offer you this License +giving you legal permission to copy, distribute and/or modify it. + + For the developers' and authors' protection, the GPL clearly explains +that there is no warranty for this free software. For both users' and +authors' sake, the GPL requires that modified versions be marked as +changed, so that their problems will not be attributed erroneously to +authors of previous versions. + + Some devices are designed to deny users access to install or run +modified versions of the software inside them, although the manufacturer +can do so. This is fundamentally incompatible with the aim of +protecting users' freedom to change the software. The systematic +pattern of such abuse occurs in the area of products for individuals to +use, which is precisely where it is most unacceptable. Therefore, we +have designed this version of the GPL to prohibit the practice for those +products. If such problems arise substantially in other domains, we +stand ready to extend this provision to those domains in future versions +of the GPL, as needed to protect the freedom of users. + + Finally, every program is threatened constantly by software patents. +States should not allow patents to restrict development and use of +software on general-purpose computers, but in those that do, we wish to +avoid the special danger that patents applied to a free program could +make it effectively proprietary. To prevent this, the GPL assures that +patents cannot be used to render the program non-free. + + The precise terms and conditions for copying, distribution and +modification follow. + + TERMS AND CONDITIONS + + 0. Definitions. + + "This License" refers to version 3 of the GNU General Public License. + + "Copyright" also means copyright-like laws that apply to other kinds of +works, such as semiconductor masks. + + "The Program" refers to any copyrightable work licensed under this +License. Each licensee is addressed as "you". "Licensees" and +"recipients" may be individuals or organizations. + + To "modify" a work means to copy from or adapt all or part of the work +in a fashion requiring copyright permission, other than the making of an +exact copy. The resulting work is called a "modified version" of the +earlier work or a work "based on" the earlier work. + + A "covered work" means either the unmodified Program or a work based +on the Program. + + To "propagate" a work means to do anything with it that, without +permission, would make you directly or secondarily liable for +infringement under applicable copyright law, except executing it on a +computer or modifying a private copy. Propagation includes copying, +distribution (with or without modification), making available to the +public, and in some countries other activities as well. + + To "convey" a work means any kind of propagation that enables other +parties to make or receive copies. Mere interaction with a user through +a computer network, with no transfer of a copy, is not conveying. + + An interactive user interface displays "Appropriate Legal Notices" +to the extent that it includes a convenient and prominently visible +feature that (1) displays an appropriate copyright notice, and (2) +tells the user that there is no warranty for the work (except to the +extent that warranties are provided), that licensees may convey the +work under this License, and how to view a copy of this License. If +the interface presents a list of user commands or options, such as a +menu, a prominent item in the list meets this criterion. + + 1. Source Code. + + The "source code" for a work means the preferred form of the work +for making modifications to it. "Object code" means any non-source +form of a work. + + A "Standard Interface" means an interface that either is an official +standard defined by a recognized standards body, or, in the case of +interfaces specified for a particular programming language, one that +is widely used among developers working in that language. + + The "System Libraries" of an executable work include anything, other +than the work as a whole, that (a) is included in the normal form of +packaging a Major Component, but which is not part of that Major +Component, and (b) serves only to enable use of the work with that +Major Component, or to implement a Standard Interface for which an +implementation is available to the public in source code form. A +"Major Component", in this context, means a major essential component +(kernel, window system, and so on) of the specific operating system +(if any) on which the executable work runs, or a compiler used to +produce the work, or an object code interpreter used to run it. + + The "Corresponding Source" for a work in object code form means all +the source code needed to generate, install, and (for an executable +work) run the object code and to modify the work, including scripts to +control those activities. However, it does not include the work's +System Libraries, or general-purpose tools or generally available free +programs which are used unmodified in performing those activities but +which are not part of the work. For example, Corresponding Source +includes interface definition files associated with source files for +the work, and the source code for shared libraries and dynamically +linked subprograms that the work is specifically designed to require, +such as by intimate data communication or control flow between those +subprograms and other parts of the work. + + The Corresponding Source need not include anything that users +can regenerate automatically from other parts of the Corresponding +Source. + + The Corresponding Source for a work in source code form is that +same work. + + 2. Basic Permissions. + + All rights granted under this License are granted for the term of +copyright on the Program, and are irrevocable provided the stated +conditions are met. This License explicitly affirms your unlimited +permission to run the unmodified Program. The output from running a +covered work is covered by this License only if the output, given its +content, constitutes a covered work. This License acknowledges your +rights of fair use or other equivalent, as provided by copyright law. + + You may make, run and propagate covered works that you do not +convey, without conditions so long as your license otherwise remains +in force. You may convey covered works to others for the sole purpose +of having them make modifications exclusively for you, or provide you +with facilities for running those works, provided that you comply with +the terms of this License in conveying all material for which you do +not control copyright. Those thus making or running the covered works +for you must do so exclusively on your behalf, under your direction +and control, on terms that prohibit them from making any copies of +your copyrighted material outside their relationship with you. + + Conveying under any other circumstances is permitted solely under +the conditions stated below. Sublicensing is not allowed; section 10 +makes it unnecessary. + + 3. Protecting Users' Legal Rights From Anti-Circumvention Law. + + No covered work shall be deemed part of an effective technological +measure under any applicable law fulfilling obligations under article +11 of the WIPO copyright treaty adopted on 20 December 1996, or +similar laws prohibiting or restricting circumvention of such +measures. + + When you convey a covered work, you waive any legal power to forbid +circumvention of technological measures to the extent such circumvention +is effected by exercising rights under this License with respect to +the covered work, and you disclaim any intention to limit operation or +modification of the work as a means of enforcing, against the work's +users, your or third parties' legal rights to forbid circumvention of +technological measures. + + 4. Conveying Verbatim Copies. + + You may convey verbatim copies of the Program's source code as you +receive it, in any medium, provided that you conspicuously and +appropriately publish on each copy an appropriate copyright notice; +keep intact all notices stating that this License and any +non-permissive terms added in accord with section 7 apply to the code; +keep intact all notices of the absence of any warranty; and give all +recipients a copy of this License along with the Program. + + You may charge any price or no price for each copy that you convey, +and you may offer support or warranty protection for a fee. + + 5. Conveying Modified Source Versions. + + You may convey a work based on the Program, or the modifications to +produce it from the Program, in the form of source code under the +terms of section 4, provided that you also meet all of these conditions: + + a) The work must carry prominent notices stating that you modified + it, and giving a relevant date. + + b) The work must carry prominent notices stating that it is + released under this License and any conditions added under section + 7. This requirement modifies the requirement in section 4 to + "keep intact all notices". + + c) You must license the entire work, as a whole, under this + License to anyone who comes into possession of a copy. This + License will therefore apply, along with any applicable section 7 + additional terms, to the whole of the work, and all its parts, + regardless of how they are packaged. This License gives no + permission to license the work in any other way, but it does not + invalidate such permission if you have separately received it. + + d) If the work has interactive user interfaces, each must display + Appropriate Legal Notices; however, if the Program has interactive + interfaces that do not display Appropriate Legal Notices, your + work need not make them do so. + + A compilation of a covered work with other separate and independent +works, which are not by their nature extensions of the covered work, +and which are not combined with it such as to form a larger program, +in or on a volume of a storage or distribution medium, is called an +"aggregate" if the compilation and its resulting copyright are not +used to limit the access or legal rights of the compilation's users +beyond what the individual works permit. Inclusion of a covered work +in an aggregate does not cause this License to apply to the other +parts of the aggregate. + + 6. Conveying Non-Source Forms. + + You may convey a covered work in object code form under the terms +of sections 4 and 5, provided that you also convey the +machine-readable Corresponding Source under the terms of this License, +in one of these ways: + + a) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by the + Corresponding Source fixed on a durable physical medium + customarily used for software interchange. + + b) Convey the object code in, or embodied in, a physical product + (including a physical distribution medium), accompanied by a + written offer, valid for at least three years and valid for as + long as you offer spare parts or customer support for that product + model, to give anyone who possesses the object code either (1) a + copy of the Corresponding Source for all the software in the + product that is covered by this License, on a durable physical + medium customarily used for software interchange, for a price no + more than your reasonable cost of physically performing this + conveying of source, or (2) access to copy the + Corresponding Source from a network server at no charge. + + c) Convey individual copies of the object code with a copy of the + written offer to provide the Corresponding Source. This + alternative is allowed only occasionally and noncommercially, and + only if you received the object code with such an offer, in accord + with subsection 6b. + + d) Convey the object code by offering access from a designated + place (gratis or for a charge), and offer equivalent access to the + Corresponding Source in the same way through the same place at no + further charge. You need not require recipients to copy the + Corresponding Source along with the object code. If the place to + copy the object code is a network server, the Corresponding Source + may be on a different server (operated by you or a third party) + that supports equivalent copying facilities, provided you maintain + clear directions next to the object code saying where to find the + Corresponding Source. Regardless of what server hosts the + Corresponding Source, you remain obligated to ensure that it is + available for as long as needed to satisfy these requirements. + + e) Convey the object code using peer-to-peer transmission, provided + you inform other peers where the object code and Corresponding + Source of the work are being offered to the general public at no + charge under subsection 6d. + + A separable portion of the object code, whose source code is excluded +from the Corresponding Source as a System Library, need not be +included in conveying the object code work. + + A "User Product" is either (1) a "consumer product", which means any +tangible personal property which is normally used for personal, family, +or household purposes, or (2) anything designed or sold for incorporation +into a dwelling. In determining whether a product is a consumer product, +doubtful cases shall be resolved in favor of coverage. For a particular +product received by a particular user, "normally used" refers to a +typical or common use of that class of product, regardless of the status +of the particular user or of the way in which the particular user +actually uses, or expects or is expected to use, the product. A product +is a consumer product regardless of whether the product has substantial +commercial, industrial or non-consumer uses, unless such uses represent +the only significant mode of use of the product. + + "Installation Information" for a User Product means any methods, +procedures, authorization keys, or other information required to install +and execute modified versions of a covered work in that User Product from +a modified version of its Corresponding Source. The information must +suffice to ensure that the continued functioning of the modified object +code is in no case prevented or interfered with solely because +modification has been made. + + If you convey an object code work under this section in, or with, or +specifically for use in, a User Product, and the conveying occurs as +part of a transaction in which the right of possession and use of the +User Product is transferred to the recipient in perpetuity or for a +fixed term (regardless of how the transaction is characterized), the +Corresponding Source conveyed under this section must be accompanied +by the Installation Information. But this requirement does not apply +if neither you nor any third party retains the ability to install +modified object code on the User Product (for example, the work has +been installed in ROM). + + The requirement to provide Installation Information does not include a +requirement to continue to provide support service, warranty, or updates +for a work that has been modified or installed by the recipient, or for +the User Product in which it has been modified or installed. Access to a +network may be denied when the modification itself materially and +adversely affects the operation of the network or violates the rules and +protocols for communication across the network. + + Corresponding Source conveyed, and Installation Information provided, +in accord with this section must be in a format that is publicly +documented (and with an implementation available to the public in +source code form), and must require no special password or key for +unpacking, reading or copying. + + 7. Additional Terms. + + "Additional permissions" are terms that supplement the terms of this +License by making exceptions from one or more of its conditions. +Additional permissions that are applicable to the entire Program shall +be treated as though they were included in this License, to the extent +that they are valid under applicable law. If additional permissions +apply only to part of the Program, that part may be used separately +under those permissions, but the entire Program remains governed by +this License without regard to the additional permissions. + + When you convey a copy of a covered work, you may at your option +remove any additional permissions from that copy, or from any part of +it. (Additional permissions may be written to require their own +removal in certain cases when you modify the work.) You may place +additional permissions on material, added by you to a covered work, +for which you have or can give appropriate copyright permission. + + Notwithstanding any other provision of this License, for material you +add to a covered work, you may (if authorized by the copyright holders of +that material) supplement the terms of this License with terms: + + a) Disclaiming warranty or limiting liability differently from the + terms of sections 15 and 16 of this License; or + + b) Requiring preservation of specified reasonable legal notices or + author attributions in that material or in the Appropriate Legal + Notices displayed by works containing it; or + + c) Prohibiting misrepresentation of the origin of that material, or + requiring that modified versions of such material be marked in + reasonable ways as different from the original version; or + + d) Limiting the use for publicity purposes of names of licensors or + authors of the material; or + + e) Declining to grant rights under trademark law for use of some + trade names, trademarks, or service marks; or + + f) Requiring indemnification of licensors and authors of that + material by anyone who conveys the material (or modified versions of + it) with contractual assumptions of liability to the recipient, for + any liability that these contractual assumptions directly impose on + those licensors and authors. + + All other non-permissive additional terms are considered "further +restrictions" within the meaning of section 10. If the Program as you +received it, or any part of it, contains a notice stating that it is +governed by this License along with a term that is a further +restriction, you may remove that term. If a license document contains +a further restriction but permits relicensing or conveying under this +License, you may add to a covered work material governed by the terms +of that license document, provided that the further restriction does +not survive such relicensing or conveying. + + If you add terms to a covered work in accord with this section, you +must place, in the relevant source files, a statement of the +additional terms that apply to those files, or a notice indicating +where to find the applicable terms. + + Additional terms, permissive or non-permissive, may be stated in the +form of a separately written license, or stated as exceptions; +the above requirements apply either way. + + 8. Termination. + + You may not propagate or modify a covered work except as expressly +provided under this License. Any attempt otherwise to propagate or +modify it is void, and will automatically terminate your rights under +this License (including any patent licenses granted under the third +paragraph of section 11). + + However, if you cease all violation of this License, then your +license from a particular copyright holder is reinstated (a) +provisionally, unless and until the copyright holder explicitly and +finally terminates your license, and (b) permanently, if the copyright +holder fails to notify you of the violation by some reasonable means +prior to 60 days after the cessation. + + Moreover, your license from a particular copyright holder is +reinstated permanently if the copyright holder notifies you of the +violation by some reasonable means, this is the first time you have +received notice of violation of this License (for any work) from that +copyright holder, and you cure the violation prior to 30 days after +your receipt of the notice. + + Termination of your rights under this section does not terminate the +licenses of parties who have received copies or rights from you under +this License. If your rights have been terminated and not permanently +reinstated, you do not qualify to receive new licenses for the same +material under section 10. + + 9. Acceptance Not Required for Having Copies. + + You are not required to accept this License in order to receive or +run a copy of the Program. Ancillary propagation of a covered work +occurring solely as a consequence of using peer-to-peer transmission +to receive a copy likewise does not require acceptance. However, +nothing other than this License grants you permission to propagate or +modify any covered work. These actions infringe copyright if you do +not accept this License. Therefore, by modifying or propagating a +covered work, you indicate your acceptance of this License to do so. + + 10. Automatic Licensing of Downstream Recipients. + + Each time you convey a covered work, the recipient automatically +receives a license from the original licensors, to run, modify and +propagate that work, subject to this License. You are not responsible +for enforcing compliance by third parties with this License. + + An "entity transaction" is a transaction transferring control of an +organization, or substantially all assets of one, or subdividing an +organization, or merging organizations. If propagation of a covered +work results from an entity transaction, each party to that +transaction who receives a copy of the work also receives whatever +licenses to the work the party's predecessor in interest had or could +give under the previous paragraph, plus a right to possession of the +Corresponding Source of the work from the predecessor in interest, if +the predecessor has it or can get it with reasonable efforts. + + You may not impose any further restrictions on the exercise of the +rights granted or affirmed under this License. For example, you may +not impose a license fee, royalty, or other charge for exercise of +rights granted under this License, and you may not initiate litigation +(including a cross-claim or counterclaim in a lawsuit) alleging that +any patent claim is infringed by making, using, selling, offering for +sale, or importing the Program or any portion of it. + + 11. Patents. + + A "contributor" is a copyright holder who authorizes use under this +License of the Program or a work on which the Program is based. The +work thus licensed is called the contributor's "contributor version". + + A contributor's "essential patent claims" are all patent claims +owned or controlled by the contributor, whether already acquired or +hereafter acquired, that would be infringed by some manner, permitted +by this License, of making, using, or selling its contributor version, +but do not include claims that would be infringed only as a +consequence of further modification of the contributor version. For +purposes of this definition, "control" includes the right to grant +patent sublicenses in a manner consistent with the requirements of +this License. + + Each contributor grants you a non-exclusive, worldwide, royalty-free +patent license under the contributor's essential patent claims, to +make, use, sell, offer for sale, import and otherwise run, modify and +propagate the contents of its contributor version. + + In the following three paragraphs, a "patent license" is any express +agreement or commitment, however denominated, not to enforce a patent +(such as an express permission to practice a patent or covenant not to +sue for patent infringement). To "grant" such a patent license to a +party means to make such an agreement or commitment not to enforce a +patent against the party. + + If you convey a covered work, knowingly relying on a patent license, +and the Corresponding Source of the work is not available for anyone +to copy, free of charge and under the terms of this License, through a +publicly available network server or other readily accessible means, +then you must either (1) cause the Corresponding Source to be so +available, or (2) arrange to deprive yourself of the benefit of the +patent license for this particular work, or (3) arrange, in a manner +consistent with the requirements of this License, to extend the patent +license to downstream recipients. "Knowingly relying" means you have +actual knowledge that, but for the patent license, your conveying the +covered work in a country, or your recipient's use of the covered work +in a country, would infringe one or more identifiable patents in that +country that you have reason to believe are valid. + + If, pursuant to or in connection with a single transaction or +arrangement, you convey, or propagate by procuring conveyance of, a +covered work, and grant a patent license to some of the parties +receiving the covered work authorizing them to use, propagate, modify +or convey a specific copy of the covered work, then the patent license +you grant is automatically extended to all recipients of the covered +work and works based on it. + + A patent license is "discriminatory" if it does not include within +the scope of its coverage, prohibits the exercise of, or is +conditioned on the non-exercise of one or more of the rights that are +specifically granted under this License. You may not convey a covered +work if you are a party to an arrangement with a third party that is +in the business of distributing software, under which you make payment +to the third party based on the extent of your activity of conveying +the work, and under which the third party grants, to any of the +parties who would receive the covered work from you, a discriminatory +patent license (a) in connection with copies of the covered work +conveyed by you (or copies made from those copies), or (b) primarily +for and in connection with specific products or compilations that +contain the covered work, unless you entered into that arrangement, +or that patent license was granted, prior to 28 March 2007. + + Nothing in this License shall be construed as excluding or limiting +any implied license or other defenses to infringement that may +otherwise be available to you under applicable patent law. + + 12. No Surrender of Others' Freedom. + + If conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot convey a +covered work so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you may +not convey it at all. For example, if you agree to terms that obligate you +to collect a royalty for further conveying from those to whom you convey +the Program, the only way you could satisfy both those terms and this +License would be to refrain entirely from conveying the Program. + + 13. Use with the GNU Affero General Public License. + + Notwithstanding any other provision of this License, you have +permission to link or combine any covered work with a work licensed +under version 3 of the GNU Affero General Public License into a single +combined work, and to convey the resulting work. The terms of this +License will continue to apply to the part which is the covered work, +but the special requirements of the GNU Affero General Public License, +section 13, concerning interaction through a network will apply to the +combination as such. + + 14. Revised Versions of this License. + + The Free Software Foundation may publish revised and/or new versions of +the GNU General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + + Each version is given a distinguishing version number. If the +Program specifies that a certain numbered version of the GNU General +Public License "or any later version" applies to it, you have the +option of following the terms and conditions either of that numbered +version or of any later version published by the Free Software +Foundation. If the Program does not specify a version number of the +GNU General Public License, you may choose any version ever published +by the Free Software Foundation. + + If the Program specifies that a proxy can decide which future +versions of the GNU General Public License can be used, that proxy's +public statement of acceptance of a version permanently authorizes you +to choose that version for the Program. + + Later license versions may give you additional or different +permissions. However, no additional obligations are imposed on any +author or copyright holder as a result of your choosing to follow a +later version. + + 15. Disclaimer of Warranty. + + THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY +APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT +HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY +OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, +THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR +PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM +IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF +ALL NECESSARY SERVICING, REPAIR OR CORRECTION. + + 16. Limitation of Liability. + + IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS +THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY +GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE +USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF +DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD +PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), +EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF +SUCH DAMAGES. + + 17. Interpretation of Sections 15 and 16. + + If the disclaimer of warranty and limitation of liability provided +above cannot be given local legal effect according to their terms, +reviewing courts shall apply local law that most closely approximates +an absolute waiver of all civil liability in connection with the +Program, unless a warranty or assumption of liability accompanies a +copy of the Program in return for a fee. + + END OF TERMS AND CONDITIONS + + How to Apply These Terms to Your New Programs + + If you develop a new program, and you want it to be of the greatest +possible use to the public, the best way to achieve this is to make it +free software which everyone can redistribute and change under these terms. + + To do so, attach the following notices to the program. It is safest +to attach them to the start of each source file to most effectively +state the exclusion of warranty; and each file should have at least +the "copyright" line and a pointer to where the full notice is found. + + <one line to give the program's name and a brief idea of what it does.> + Copyright (C) <year> <name of author> + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see <https://www.gnu.org/licenses/>. + +Also add information on how to contact you by electronic and paper mail. + + If the program does terminal interaction, make it output a short +notice like this when it starts in an interactive mode: + + <program> Copyright (C) <year> <name of author> + This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. + This is free software, and you are welcome to redistribute it + under certain conditions; type `show c' for details. + +The hypothetical commands `show w' and `show c' should show the appropriate +parts of the General Public License. Of course, your program's commands +might be different; for a GUI interface, you would use an "about box". + + You should also get your employer (if you work as a programmer) or school, +if any, to sign a "copyright disclaimer" for the program, if necessary. +For more information on this, and how to apply and follow the GNU GPL, see +<https://www.gnu.org/licenses/>. + + The GNU General Public License does not permit incorporating your program +into proprietary programs. If your program is a subroutine library, you +may consider it more useful to permit linking proprietary applications with +the library. If this is what you want to do, use the GNU Lesser General +Public License instead of this License. But first, please read +<https://www.gnu.org/licenses/why-not-lgpl.html>. diff --git a/proofsearch/README.md b/proofsearch/README.md new file mode 100644 index 0000000..ac0ccd6 --- /dev/null +++ b/proofsearch/README.md @@ -0,0 +1,49 @@ +# ATP Engine + +A saturation-based automated theorem prover for first-order logic, written in C++20. + +## Overview + +ATP Engine implements the **Given Clause Loop** (Otter/E-style) with hash-consed term sharing, discrimination tree indexing, and pluggable search heuristics. It reads problems in [TPTP](https://www.tptp.org/) format and produces human-readable proofs via resolution and factoring. + +The architecture is designed for extensibility toward equality reasoning (superposition), sorted logic, and theory integration. See [`docs/architecture.md`](docs/architecture.md) for full design documentation. + +## Build + +Requires CMake 3.20+ and a C++20 compiler (GCC 11+ / Clang 14+). + +```bash +cmake -B build -DCMAKE_BUILD_TYPE=Debug +cmake --build build -j$(nproc) +``` + +### Options + +| Flag | Default | Description | +|------|---------|-------------| +| `ATP_ENABLE_CLANG_TIDY` | `OFF` | Run clang-tidy during compilation | +| `ATP_ENABLE_SANITIZERS` | `ON` | ASan + UBSan in Debug builds | +| `ATP_BUILD_TESTS` | `ON` | Build GoogleTest unit tests | + +### Format & Lint + +```bash +cmake --build build --target format # auto-format all sources +cmake --build build --target format-check # check format compliance +``` + +## Run + +```bash +./build/atp data/monkey_banana.p +``` + +## Test + +```bash +cd build && ctest --output-on-failure +``` + +## License + +This project is licensed under the [GNU General Public License v3.0](https://www.gnu.org/licenses/gpl-3.0.html). Also see [LICENSE](LICENSE) diff --git a/proofsearch/data/monkey_banana.p b/proofsearch/data/monkey_banana.p new file mode 100644 index 0000000..446c20a --- /dev/null +++ b/proofsearch/data/monkey_banana.p @@ -0,0 +1,27 @@ +% ========================================================================= +% Monkey and Banana Problem +% State representation: state(Monkey, Box, Banana, Height, Situation) +% ========================================================================= + +% 1. Initial state (corresponding sample input: A B C 0) +cnf(init_state, axiom, state(a, b, c, h0, s0)). + +% 2. State transition axioms (action rules) +% Action: Go(X) +cnf(action_go, axiom, ~state(M, B, G, h0, S) | state(X, B, G, h0, do(go(X), S)) ). + +% Action: Push(X) (Note M and B use the same variable M representing M=B) +cnf(action_push, axiom, ~state(M, M, G, h0, S) | state(X, X, G, h0, do(push(X), S)) ). + +% Action: Climb() +cnf(action_climb, axiom, ~state(M, M, G, h0, S) | state(M, M, G, h1, do(climb, S)) ). + +% Action: Down() +cnf(action_down, axiom, ~state(M, B, G, h1, S) | state(M, B, G, h0, do(down, S)) ). + +% Action: Reach() (Note M, B, G all use G uniformly, representing M=G and B=G) +cnf(action_reach, axiom, ~state(G, G, G, h1, S) | goal_reached(do(reach, S)) ). + +% 3. Goal theorem (using proof by contradiction) +% Goal: There exists a state S such that goal_reached(S) is true. +cnf(negated_goal, negated_conjecture, ~goal_reached(S) ).
\ No newline at end of file diff --git a/proofsearch/data/simple_propositional.p b/proofsearch/data/simple_propositional.p new file mode 100644 index 0000000..283c326 --- /dev/null +++ b/proofsearch/data/simple_propositional.p @@ -0,0 +1,5 @@ +% Simple propositional-style test +% P(a) and (P(X) → Q(X)) and ¬Q(a) should be unsatisfiable. +cnf(fact, axiom, p(a)). +cnf(rule, axiom, ~p(X) | q(X)). +cnf(goal, negated_conjecture, ~q(a)). diff --git a/proofsearch/docs/architecture.md b/proofsearch/docs/architecture.md new file mode 100644 index 0000000..333fa99 --- /dev/null +++ b/proofsearch/docs/architecture.md @@ -0,0 +1,630 @@ +# ATP Engine — Architecture Design Document + +> **Version**: 1.0 +> **Target**: Extensible first-order logic theorem prover (saturation-based) +> **Language**: C++20 +> **Build**: CMake 3.20+, GoogleTest, ANTLR4 (C++ target) + +--- + +## Table of Contents + +1. [Design Philosophy](#1-design-philosophy) +2. [System Architecture](#2-system-architecture) +3. [Directory Structure](#3-directory-structure) +4. [Module Specifications](#4-module-specifications) +5. [Data Flow](#5-data-flow) +6. [Known Limitations & Future Work](#6-known-limitations--future-work) +7. [References](#7-references) + +--- + +## 1. Design Philosophy + +### 1.1 Core Principles + +| Principle | Rationale | +|-----------|-----------| +| **Bottom-up construction** | Build from the memory layer upward. A stable Term Bank is the foundation everything else rests on. | +| **Strict layered dependencies** | Dependencies flow in one direction only: `core → infer → index → simplify → search → proof`. No cycles. | +| **Interface-implementation separation** | Headers in `include/atp/` define interfaces; `src/` contains implementations. Modules communicate through stable APIs. | +| **Premature abstraction avoidance** | V1 hardcodes resolution + factoring. Abstract strategy selection (`strategy/`) is scaffolded but not wired in until V2. | +| **Parse once, reason forever** | Text parsing (ANTLR4) is a one-shot frontend concern. The core engine operates entirely on integer IDs, never on strings. | + +### 1.2 Design Influences + +This architecture draws from three production-grade theorem provers: + +- **E Prover** (Stephan Schulz) — Given Clause Loop, term sharing via hash consing, age-weight clause selection. +- **Vampire** (Andrei Voronkov et al.) — AVATAR splitting, superposition calculus, discrimination tree indexing. +- **Otter** (William McCune) — Original set-of-support strategy, subsumption, demodulation. + +### 1.3 Versioning Strategy + +``` +V1 → Pure first-order resolution (no equality). Solve the Monkey-Banana problem. +V2 → Pluggable inference rules (Calculus), age-weight scheduling, variable standardization. +V3 → Equality reasoning (paramodulation/superposition), term orderings (KBO/LPO). +V4 → AVATAR splitting, SAT solver integration, TPTP competition readiness. +``` + +--- + +## 2. System Architecture + +### 2.1 Layered Architecture Overview + +``` +┌──────────────────────────────────────────────────────────────────────┐ +│ Frontend Layer │ +│ TPTP File → ANTLR4 Lexer/Parser → AST Builder → tptp_parser.h │ +└────────────────────────────────┬─────────────────────────────────────┘ + │ Formula (internal AST) +┌────────────────────────────────▼─────────────────────────────────────┐ +│ Normalization Layer │ +│ formula.h → clausifier.h (NNF → Skolem → CNF) │ +└────────────────────────────────┬─────────────────────────────────────┘ + │ Clause set +┌────────────────────────────────▼─────────────────────────────────────┐ +│ Search Layer (Control) │ +│ │ +│ ┌──────────────┐ select ┌─────────────────┐ resolve with all │ +│ │ Unprocessed │─────────→ │ Given Clause │─────────────────→ │ +│ │ (pri queue) │ │ (selected) │ │ +│ └──────▲───────┘ └─────────────────┘ │ +│ │ enqueue survivors │ +│ ┌──────┴───────┐ ┌─────────────────┐ │ +│ │ Simplify & │←──────────│ New Clauses │ │ +│ │ Filter │ │ (resolvents) │ │ +│ └──────────────┘ └─────────────────┘ │ +│ │ if empty clause found │ +└──────────┼───────────────────────────────────────────────────────────┘ + ▼ +┌──────────────────────────────────────────────────────────────────────┐ +│ Output Layer │ +│ proof_trace.h → DFS backtrack → format & print action sequence │ +└──────────────────────────────────────────────────────────────────────┘ + +═══════════════════════ Shared Foundation ══════════════════════════════ +┌──────────────────────────────────────────────────────────────────────┐ +│ Core Layer (Data Plane) │ +│ Symbol Table │ Term Bank (hash consing) │ Clause Store │ Types │ +└──────────────────────────────────────────────────────────────────────┘ +``` + +### 2.2 Dependency Graph + +``` +frontend ──→ normalize ──→ core + ↑ +search ──→ simplify ──→ index ──→ infer ──→ core + ↑ + rewrite ─┘ + proof ──→ core/clause_store + + strategy/ ──→ (V2: wired into search) +``` + +All arrows point downward/inward. `proof` depends only on `clause_store`, not on `search` (no reverse dependency). + +--- + +## 3. Directory Structure + +``` +richard-atp-engine/ +├── CMakeLists.txt # Top-level build (C++20, clang-tidy, clang-format, sanitizers) +├── .clang-format # Google-based, 4-space indent, 100-col +├── .clang-tidy # Strict checks, filtered for generated code +├── .gitignore +│ +├── grammar/ +│ └── TPTP.g4 # ANTLR4 grammar for TPTP fof/cnf syntax +│ +├── docs/ +│ └── architecture.md # This document +│ +├── data/ +│ └── monkey_banana.p # First integration test (TPTP format) +│ +├── include/atp/ +│ ├── core/ # Data plane — memory foundation +│ │ ├── types.h # TermId, ClauseId, SymbolId, SortId, SymbolKind, InferenceRule +│ │ ├── symbol_table.h # String interning with kind/sort metadata +│ │ ├── term.h # Flat term struct (symbol_id + args) +│ │ ├── literal.h # Polarity + atom TermId +│ │ ├── clause.h # Literal vector + provenance (parents, rule, depth) +│ │ ├── clause_store.h # Central clause ownership, ClauseId allocation +│ │ └── term_bank.h # Hash-consing pool for structural sharing +│ │ +│ ├── normalize/ # Normalization — FOL formula to CNF +│ │ ├── formula.h # FOL AST nodes (And, Or, Not, Forall, Exists, ...) +│ │ └── clausifier.h # Eliminate →/↔ → NNF → Skolemize → distribute → flatten +│ │ +│ ├── infer/ # Compute plane — stateless inference operators +│ │ ├── substitution.h # Variable binding map (stack-lifetime) +│ │ ├── unification.h # MGU with optional occurs check +│ │ └── resolution.h # Binary resolution + factoring +│ │ +│ ├── index/ # Index plane — fast term retrieval +│ │ └── discrim_tree.h # Discrimination tree (unifiable / instance / generalization queries) +│ │ +│ ├── simplify/ # Redundancy elimination +│ │ ├── tautology.h # Complementary literal detection +│ │ └── subsumption.h # Forward/backward subsumption (backed by discrim tree) +│ │ +│ ├── search/ # Control plane — proof search scheduling +│ │ ├── clause_queue.h # Comparators (BFS, weight-based) +│ │ └── prover.h # Given Clause Loop (V1: hardcoded rules; V2: Calculus-driven) +│ │ +│ ├── proof/ # Output — proof reconstruction +│ │ └── proof_trace.h # DFS backtrack from empty clause, formatting +│ │ +│ ├── rewrite/ # Equality reasoning (V3 extension point) +│ │ ├── ordering.h # Abstract TermOrdering (KBO, LPO) +│ │ └── paramodulation.h # Paramodulation + demodulation +│ │ +│ ├── strategy/ # Dynamic algorithm selection (V2 extension point) +│ │ ├── inference_rule.h # GeneratingRule / SimplifyingRule interfaces +│ │ ├── calculus.h # Bundles rules + heuristics + ordering +│ │ └── problem_analyzer.h # Feature detection + calculus selection +│ │ +│ └── utils/ +│ ├── hash_utils.h # Hash combination (boost::hash_combine equivalent) +│ └── logger.h # Compile-time-filtered logging macros +│ +├── src/ # Implementation files (mirror include/ structure) +│ ├── core/ +│ ├── normalize/ +│ ├── infer/ +│ ├── index/ +│ ├── simplify/ +│ ├── search/ +│ ├── proof/ +│ ├── rewrite/ +│ ├── strategy/ +│ ├── frontend/ +│ └── main.cpp +│ +└── tests/ # GoogleTest unit tests + ├── CMakeLists.txt + ├── test_term_bank.cc + ├── test_unification.cc + ├── test_clausifier.cc + ├── test_resolution.cc + ├── test_discrim_tree.cc + └── test_prover.cc # End-to-end: Monkey-Banana problem +``` + +--- + +## 4. Module Specifications + +### 4.1 Core Layer (`core/`) + +The core layer owns all persistent data. Every other module receives `const&` or `&` references to core objects — never raw pointers, never ownership. + +#### `types.h` — Type System Foundation + +```cpp +using SymbolId = uint32_t; // Index into SymbolTable +using TermId = uint32_t; // Index into TermBank (hash-consed) +using ClauseId = uint32_t; // Index into ClauseStore +using SortId = uint16_t; // For sorted logic (V3+), default = kUnsorted + +enum class SymbolKind : uint8_t { + kVariable, kConstant, kFunction, kPredicate, kSkolem +}; + +enum class InferenceRule : uint16_t { + kInput = 0, kResolution = 1, kFactoring = 2, // Core + kParamodulation = 100, kDemodulation = 101, ... // Equality (V3) + kSubsumption = 200, kTautologyElim = 201, ... // Simplification + kTheoryResolution = 300, ... // Theory (V4) +}; +``` + +**Design decisions**: +- `uint32_t` IDs instead of pointers — enables flat array storage, trivial comparison, and cache-friendly iteration. +- `InferenceRule` uses `uint16_t` with reserved ranges (0-99 core, 100-199 equality, 200-299 simplification, 300+ theory) to avoid enum churn as the system grows. +- `SymbolKind` enables distinguishing variables from function symbols at the symbol level, critical for unification and sorted logic. +- `SortId` is present but unused in V1 (`kUnsorted`), ready for sorted unification in V3. + +#### `symbol_table.h` — String Interning + +```cpp +struct SymbolInfo { + std::string name; + SymbolKind kind; + uint16_t arity; + SortId sort; +}; + +class SymbolTable { + SymbolId intern(string_view name, SymbolKind kind, uint16_t arity, SortId sort); + string_view getName(SymbolId id) const; + const SymbolInfo& getInfo(SymbolId id) const; + bool isVariable(SymbolId id) const; +}; +``` + +Each unique symbol string is stored exactly once. All downstream modules work with `SymbolId` integers. The `SymbolInfo` metadata (kind, arity, sort) enables type-checking during unification without string inspection. + +#### `term_bank.h` — Hash Consing + +```cpp +class TermBank { + TermId makeTerm(SymbolId symbol, span<const TermId> args); + TermId makeVar(SymbolId var_symbol); + const Term& getTerm(TermId id) const; + bool isVariable(TermId id) const; +}; +``` + +**Hash consing guarantee**: If `makeTerm(f, {a, b})` is called twice with the same `f`, `a`, `b`, it returns the same `TermId`. This makes structural equality a single integer comparison (`O(1)`), which is the foundation for efficient indexing and subsumption. + +**Memory layout**: Terms are stored in a flat arena. Each `Term` header (`symbol_id` + `arity`) is followed by its argument `TermId` array in contiguous memory. No heap allocation per term. + +#### `clause_store.h` — Clause Ownership + +```cpp +class ClauseStore { + ClauseId addClause(Clause clause); + const Clause& getClause(ClauseId id) const; + Clause& getMutableClause(ClauseId id); + void forEach(const function<void(const Clause&)>& visitor) const; +}; +``` + +Separated from `Prover` so that proof extraction, simplification, and search all access clauses through the same stable interface. Changing the search strategy (OTTER loop → DISCOUNT loop) does not affect clause storage. + +--- + +### 4.2 Normalization Layer (`normalize/`) + +#### `formula.h` — First-Order Logic AST + +```cpp +enum class FormulaKind : uint8_t { + kAtom, kNot, kAnd, kOr, kImplies, kIff, kForall, kExists +}; + +struct Formula { + FormulaKind kind; + TermId atom; // for kAtom + string var_name; // for quantifiers + vector<unique_ptr<Formula>> children; // sub-formulas +}; +``` + +This is the **pre-clausification** representation. The parser builds `Formula` trees; the clausifier destroys them and produces `Clause` vectors. Formula nodes are short-lived — they exist only during the normalization phase. + +#### `clausifier.h` — CNF Conversion Pipeline + +``` +Input Formula + │ + ▼ eliminateImplication() — P → Q becomes ¬P ∨ Q + ▼ eliminateBiconditional() — P ↔ Q becomes (¬P ∨ Q) ∧ (P ∨ ¬Q) + ▼ pushNegation() — ¬(P ∧ Q) becomes ¬P ∨ ¬Q (NNF) + ▼ skolemize() — ∀x∃y.P(x,y) becomes ∀x.P(x, sk(x)) + ▼ dropUniversal() — All remaining vars are implicitly ∀ + ▼ distribute() — (P ∨ (Q ∧ R)) becomes (P ∨ Q) ∧ (P ∨ R) + ▼ flatten() — Nested ∧ at top level → separate clauses + │ + ▼ +Output: vector<Clause> +``` + +**Critical**: `skolemize()` must correctly handle nested quantifier scopes. Given `∀x ∃y ∀z ∃w. P(x,y,z,w)`, the Skolem functions are `y = sk1(x)` and `w = sk2(x, z)` — each existential variable becomes a function of all universally quantified variables in its scope. + +--- + +### 4.3 Inference Layer (`infer/`) + +#### `substitution.h` — Variable Bindings + +A substitution `σ = {X → f(a), Y → Z}` maps variables to terms. Key properties: + +- **Stack lifetime**: Created during unification, applied to build the resolvent, then discarded. Never stored long-term. +- **Chain resolution**: `resolve(X)` walks the binding chain (`X → Y → f(a)`) to the final value. +- **Idempotence**: After applying a substitution, no variables in the result have bindings in the same substitution. + +#### `unification.h` — Most General Unifier + +```cpp +bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, + const UnificationConfig& config); +``` + +The Robinson unification algorithm, operating on `TermId` values via the `TermBank`. Returns the Most General Unifier (MGU) if one exists. + +**Occurs check**: Configurable via `UnificationConfig::enable_occurs_check`. Disabled for situation calculus planning (performance); enabled for general mathematical reasoning (soundness — prevents infinite terms like `X = f(X)`). + +#### `resolution.h` — Inference Rules + +```cpp +optional<Clause> resolve(bank, clause1, lit_idx1, clause2, lit_idx2); +vector<Clause> allResolvents(bank, clause1, clause2); +vector<Clause> factor(bank, clause); +``` + +**Binary resolution**: Given clauses `{P(x), Q(x)}` and `{¬P(a), R(a)}`, if `P(x)` and `P(a)` unify under `σ = {x→a}`, produce resolvent `{Q(a), R(a)}`. + +**Factoring**: Given clause `{P(x), P(a), Q(x)}`, if `P(x)` and `P(a)` unify, produce `{P(a), Q(a)}`. Factoring is necessary for completeness of binary resolution. + +--- + +### 4.4 Index Layer (`index/`) + +#### `discrim_tree.h` — Discrimination Tree + +A trie-based index over the flattened structure of terms. Supports three query types: + +| Query | Use Case | Direction | +|-------|----------|-----------| +| `queryUnifiable(t)` | Find resolution partners | Bidirectional matching | +| `queryInstances(t)` | Backward subsumption | Pattern more general than indexed | +| `queryGeneralizations(t)` | Forward subsumption | Indexed more general than query | + +The tree is built by linearizing terms in pre-order: `f(g(a), b)` becomes the key sequence `[f, g, a, *, b]` where `*` represents a variable (wildcard). Lookups traverse the trie, branching at decision points. + +--- + +### 4.5 Simplification Layer (`simplify/`) + +#### `tautology.h` + +Detects clauses containing both `P` and `¬P` for the same atom. These are logically true and can be safely discarded without affecting completeness. + +#### `subsumption.h` + +Backed by the discrimination tree. Two operations: + +- **Forward subsumption**: Before enqueuing a new clause `C`, check if any existing clause `D` subsumes it (`D ⊆ C` — every literal of `D` matches a literal of `C`). If yes, discard `C`. +- **Backward subsumption**: After adding `C`, check if `C` subsumes any existing clause `D`. If yes, remove `D`. + +Subsumption is the single most important simplification rule for keeping the clause set manageable. + +--- + +### 4.6 Search Layer (`search/`) + +#### `prover.h` — The Given Clause Loop + +The main proof search loop, following the OTTER/E paradigm: + +``` +procedure GivenClauseLoop(initial_clauses): + Unprocessed ← priority_queue(initial_clauses) + Processed ← empty_set + + while Unprocessed is not empty: + given ← Unprocessed.pop() // clause selection + + if given is tautology: continue + if given is forward-subsumed: continue + + // Backward simplification + remove from Processed all clauses subsumed by given + + // Inference + for each clause C in Processed: + for each resolvent R of (given, C): + if R is empty clause: RETURN PROOF FOUND + if R is not tautology and not forward-subsumed: + Unprocessed.push(R) + + // Generate factors of given + for each factor F of given: + if F is empty clause: RETURN PROOF FOUND + Unprocessed.push(F) + + Processed.add(given) + + RETURN SATURATED (no proof exists) +``` + +**V1 configuration**: +```cpp +struct ProverConfig { + ClauseComparator comparator = bfsCompare; // BFS for shortest proof + size_t max_clauses = 100000; + size_t max_iterations = 500000; + bool enable_occurs_check = false; +}; +``` + +--- + +### 4.7 Proof Layer (`proof/`) + +#### `proof_trace.h` + +When the empty clause `□` is derived, the prover halts. Proof extraction walks the `parent1`/`parent2` pointers stored in each `Clause` via DFS, reconstructing the derivation tree from `□` back to input axioms. + +The output is a sequence of `ProofStep` records, each containing the inference rule used and the parent clause IDs. This can be formatted as a human-readable proof or (future) TSTP-compliant output. + +--- + +### 4.8 Extension Point: Rewriting (`rewrite/`) + +Scaffolded for V3. Not compiled in V1. + +#### `ordering.h` — Abstract Term Ordering + +```cpp +class TermOrdering { + virtual OrderResult compare(const TermBank& bank, TermId t1, TermId t2) const = 0; +}; +``` + +Concrete implementations (future): Knuth-Bendix Ordering (KBO), Lexicographic Path Ordering (LPO). These are required for ordered resolution and superposition calculus — they ensure that rewriting always terminates. + +#### `paramodulation.h` — Equality Reasoning + +Paramodulation replaces a subterm in one clause with an equal term from another. Combined with a term ordering, this becomes the **superposition calculus** — the dominant approach for first-order logic with equality. + +--- + +### 4.9 Extension Point: Strategy (`strategy/`) + +Scaffolded for V2. Not compiled in V1. + +The strategy module will enable dynamic algorithm selection based on problem analysis: + +``` +Input clauses → ProblemAnalyzer → ProblemFeatures → selectCalculus() → Calculus + │ + ┌────────────────────────────────────────────────┘ + ▼ + Calculus = { generating_rules[], simplifying_rules[], + comparator, ordering, resource_limits } + │ + ▼ + Prover.prove(calculus) +``` + +This prevents search space explosion by loading only the inference rules relevant to the problem. A pure propositional problem would never load the paramodulation rule; an equality-heavy problem would skip pure resolution in favor of superposition. + +--- + +## 5. Data Flow + +### 5.1 End-to-End Pipeline + +``` +monkey_banana.p (TPTP text file) + │ + ▼ + [tptp_parser] ANTLR4 lexer/parser → parse tree → Formula AST + │ + ▼ + [clausifier] NNF → Skolemize → CNF → vector<Clause> + │ + ▼ + [prover] Given Clause Loop (resolution + factoring + subsumption) + │ + ├── Normal: derive new clauses, enqueue, repeat + │ + └── Empty clause found! + │ + ▼ + [proof_trace] DFS backtrack through parent pointers + │ + ▼ + Human-readable proof output +``` + +### 5.2 Term Lifecycle + +``` +String "do(walk, S0)" + │ + ▼ SymbolTable::intern() + SymbolIds: { do=0, walk=1, S0=2 } + │ + ▼ TermBank::makeTerm() + TermIds: S0_term=0, walk_term=1, do_walk_S0=2 + │ (hash-consed: calling makeTerm(do, [walk, S0]) again returns 2) + │ + ▼ Used everywhere as integer IDs + Clause { literals: [ Literal{atom=2, positive=true} ] } +``` + +### 5.3 Substitution Lifecycle + +``` +Unify( P(X, f(Y)), P(a, f(b)) ) + │ + ▼ unify() creates stack-local Substitution + σ = { X → a, Y → b } + │ + ▼ Apply σ to build resolvent clause + New terms created in TermBank (hash-consed) + │ + ▼ Substitution goes out of scope — destroyed + Only the new TermIds persist +``` + +--- + +## 6. Known Limitations & Future Work + +### 6.1 Critical Gaps (Ordered by Priority) + +#### Gap 1: No Variable Standardization Apart + +**Impact**: Correctness bug if not addressed before first real resolution. + +When resolving clause `{P(X)}` with clause `{¬P(X), Q(X)}`, variable `X` in the two clauses must be treated as distinct. Without renaming one clause's variables (e.g., `X → X'`), the unifier incorrectly constrains both clauses' variables. + +**Fix**: Add `renameVariables(Clause&, TermBank&, uint32_t& next_var_id)` to `infer/` before Phase 2 resolution implementation. + +#### Gap 2: No Literal Selection Function + +**Impact**: Search space is ~10x larger than necessary. + +Ordered resolution restricts inference to the **maximal literal** (under a term ordering) in each clause. Our `Prover` currently has no concept of selecting which literal to resolve on — it tries all pairs. + +**Fix**: V2 — add `LiteralSelector` interface, parameterized by `TermOrdering`. + +#### Gap 3: Single Clause Queue (No Age-Weight Interleaving) + +**Impact**: Incomplete or extremely slow on hard problems. + +A single `ClauseComparator` cannot implement the age-weight ratio that E Prover uses: "pick the lightest clause 5 times, then the oldest clause once." This interleaving is crucial for both performance and completeness. + +**Fix**: V2 — replace `ClauseComparator` with a `ClauseQueue` abstract class supporting multi-queue round-robin. + +#### Gap 4: Single Index Type + +**Impact**: Suboptimal retrieval performance. + +The discrimination tree handles forward matching well but is not ideal for all query patterns. Modern ATPs maintain multiple complementary indices: + +| Index Type | Best For | +|-----------|----------| +| Discrimination Tree | Forward matching (generalization queries) | +| Substitution Tree | Backward matching + unification candidates | +| Fingerprint Index | O(1) pre-filtering of non-unifiable pairs | +| Feature Vector Index | Clause-level subsumption checks | + +**Fix**: V3 — abstract `TermIndex` interface, multiple implementations. + +#### Gap 5: No Preprocessing Pipeline + +**Impact**: Missed optimization opportunities. + +Between clausification and the main loop, modern ATPs perform definition unfolding, pure literal elimination, equality axiom injection, and miniscoping. Our `normalize/` layer has only the clausifier. + +**Fix**: V2 — extend `normalize/` into a transform pipeline with pluggable passes. + +#### Gap 6: No AVATAR Splitting + +**Impact**: Cannot compete on structured problems. + +AVATAR splits clauses with independent variable sets into propositional components managed by an embedded SAT solver. This is the single largest performance innovation in ATP in the last decade (10-100x speedup on structured problems). + +**Fix**: V4 — add `sat/` module with MiniSat/CaDiCaL integration + splitting logic in `search/`. + +### 6.2 Non-Critical Gaps + +| Gap | Category | Target Version | +|-----|----------|----------------| +| TSTP proof output format | Interoperability | V2 | +| Watched literals for unit propagation | Performance | V3 | +| Clause arena (replace `vector<Literal>`) | Memory | V3 | +| ML-guided clause selection | Research | V5+ | +| Parallel portfolio mode | Performance | V5+ | + +--- + +## 7. References + +1. Schulz, S. (2013). *System Description: E 1.8*. CADE-24. +2. Kovács, L., Voronkov, A. (2013). *First-Order Theorem Proving and Vampire*. CAV 2013. +3. Voronkov, A. (2014). *AVATAR: The Architecture for First-Order Theorem Provers*. CAV 2014. +4. Nieuwenhuis, R., Rubio, A. (2001). *Paramodulation-Based Theorem Proving*. Handbook of Automated Reasoning. +5. Sutcliffe, G. (2009). *The TPTP Problem Library and Associated Infrastructure*. Journal of Automated Reasoning. +6. Robinson, J.A. (1965). *A Machine-Oriented Logic Based on the Resolution Principle*. JACM. diff --git a/proofsearch/grammar/TPTP.g4 b/proofsearch/grammar/TPTP.g4 new file mode 100644 index 0000000..e69de29 --- /dev/null +++ b/proofsearch/grammar/TPTP.g4 diff --git a/proofsearch/include/atp/core/clause.h b/proofsearch/include/atp/core/clause.h new file mode 100644 index 0000000..6387adf --- /dev/null +++ b/proofsearch/include/atp/core/clause.h @@ -0,0 +1,52 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file clause.h +/// @brief A clause is a disjunction of literals, with provenance tracking. +/// +/// NOTE: V1 uses std::vector<Literal> for simplicity. +/// Future optimization: migrate to a Clause Arena with contiguous storage. + +#include "atp/core/literal.h" +#include "atp/core/types.h" + +#include <vector> + +namespace atp { + +/// A clause: a disjunction of literals plus provenance for proof reconstruction. +struct Clause { + ClauseId id_ = kInvalidId; + std::vector<Literal> literals_; + + // Provenance (for proof trace) + InferenceRule rule_ = InferenceRule::kInput; + ClauseId parent1_ = kInvalidId; + ClauseId parent2_ = kInvalidId; + uint16_t depth_ = 0; ///< Derivation depth (for BFS scheduling) + + /// True if the clause has no literals (contradiction). + [[nodiscard]] bool isEmpty() const { return literals_.empty(); } + + /// Number of literals. + [[nodiscard]] size_t size() const { return literals_.size(); } +}; + +} // namespace atp diff --git a/proofsearch/include/atp/core/clause_store.h b/proofsearch/include/atp/core/clause_store.h new file mode 100644 index 0000000..5d6562a --- /dev/null +++ b/proofsearch/include/atp/core/clause_store.h @@ -0,0 +1,64 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file clause_store.h +/// @brief Central clause storage — owns all clauses, assigns ClauseIds. +/// +/// Extracted from Prover to separate storage responsibility from search logic. +/// This enables swapping search strategies (OTTER loop / DISCOUNT loop) +/// without touching clause lifecycle management. + +#include "atp/core/clause.h" +#include "atp/core/types.h" + +#include <functional> +#include <vector> + +namespace atp { + +/// Central clause store. Owns all clauses and assigns unique ClauseIds. +/// All modules access clauses through this store via ClauseId references. +class ClauseStore { + public: + ClauseStore() = default; + + /// Add a clause, assign it a ClauseId, and return the ID. + ClauseId addClause(Clause clause); + + /// Access a clause by its ID. UB if id is out of range. + [[nodiscard]] const Clause& getClause(ClauseId id) const; + + /// Mutable access (for marking clauses as deleted, etc.) + [[nodiscard]] Clause& getMutableClause(ClauseId id); + + /// Total number of stored clauses. + [[nodiscard]] size_t size() const; + + /// Iterate over all clauses with a visitor. + void forEach(const std::function<void(const Clause&)>& visitor) const; + // function may have type erasure overhead, consider using a template + // template <typename Visitor> + // void forEach(Visitor&& visitor) const; + + private: + std::vector<Clause> clauses_; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/core/literal.h b/proofsearch/include/atp/core/literal.h new file mode 100644 index 0000000..e58b185 --- /dev/null +++ b/proofsearch/include/atp/core/literal.h @@ -0,0 +1,39 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file literal.h +/// @brief A literal is a (possibly negated) atomic formula. + +#include "atp/core/types.h" + +namespace atp { + +/// A literal: a polarity flag plus the TermId of the atom. +struct Literal { + TermId atom_; ///< TermId of the predicate application + bool is_positive_; ///< true = positive, false = negated + + /// Complement: flip polarity, same atom. + [[nodiscard]] Literal complement() const { return {.atom_ = atom_, .is_positive_ = !is_positive_}; } + + bool operator==(const Literal& other) const = default; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/core/symbol_table.h b/proofsearch/include/atp/core/symbol_table.h new file mode 100644 index 0000000..a646f78 --- /dev/null +++ b/proofsearch/include/atp/core/symbol_table.h @@ -0,0 +1,71 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file symbol_table.h +/// @brief Bidirectional mapping between symbol names and SymbolIds, +/// with kind and sort metadata. + +#include "atp/core/types.h" + +#include <deque> +#include <string> +#include <string_view> +#include <unordered_map> + +namespace atp { + +/// Metadata associated with an interned symbol. +struct SymbolInfo { + std::string name_; + SymbolKind kind_ = SymbolKind::kFunction; + uint16_t arity_ = 0; + SortId sort_ = kUnsorted; ///< Result sort (for sorted logic) +}; + +/// Interns symbol names so that each unique string is stored exactly once. +/// Also tracks symbol metadata (kind, arity, sort). +/// Thread-safety: NOT thread-safe (single-threaded prover design). +class SymbolTable { + public: + SymbolTable() = default; + + /// Intern a symbol name with metadata. Returns existing ID if already present. + SymbolId intern(std::string_view name, SymbolKind kind, uint16_t arity = 0, + SortId sort = kUnsorted); + + /// Look up the name for a given SymbolId. UB if id is out of range. + [[nodiscard]] std::string_view getName(SymbolId id) const; + + /// Look up full metadata for a SymbolId. + [[nodiscard]] const SymbolInfo& getInfo(SymbolId id) const; + + /// Check if a symbol is a variable. + [[nodiscard]] bool isVariable(SymbolId id) const; + + /// Number of interned symbols. + [[nodiscard]] size_t size() const; + + private: + // TODO: Phase 1 implementation + std::deque<SymbolInfo> infos_; + std::unordered_map<std::string_view, SymbolId> name_to_id_; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/core/term.h b/proofsearch/include/atp/core/term.h new file mode 100644 index 0000000..d35c753 --- /dev/null +++ b/proofsearch/include/atp/core/term.h @@ -0,0 +1,43 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file term.h +/// @brief Core Term data structure — hash-consed, immutable. +/// +/// V1 uses vector<TermId> for args. +/// Future: flat arena with contiguous arg storage for cache locality. + +#include "atp/core/types.h" + +#include <vector> + +namespace atp { + +/// A term is a function/predicate application: f(t1, t2, ..., tn). +/// Variables are 0-arity terms whose symbol has SymbolKind::kVariable. +struct Term { + SymbolId symbol_id_; ///< Index into the SymbolTable + std::vector<TermId> args_; ///< Argument sub-term IDs + + /// Number of arguments. + [[nodiscard]] uint16_t arity() const { return static_cast<uint16_t>(args_.size()); } +}; + +} // namespace atp diff --git a/proofsearch/include/atp/core/term_bank.h b/proofsearch/include/atp/core/term_bank.h new file mode 100644 index 0000000..ca12759 --- /dev/null +++ b/proofsearch/include/atp/core/term_bank.h @@ -0,0 +1,86 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file term_bank.h +/// @brief Hash-consing term pool — guarantees structural sharing. + +#include "atp/core/symbol_table.h" +#include "atp/core/term.h" +#include "atp/core/types.h" + +#include <span> +#include <unordered_map> +#include <vector> + +namespace atp { + +/// Global term pool with hash-consing. +/// Every structurally identical term maps to the same TermId. +/// +/// Holds a reference to SymbolTable for variable detection. +class TermBank { + public: + /// TermBank needs the SymbolTable to distinguish variables from constants + /// (both have 0 args, but SymbolKind differs). + explicit TermBank(SymbolTable& symbols) : symbols_(&symbols) {} + + /// Create or retrieve a term. Returns the canonical TermId. + TermId makeTerm(SymbolId symbol, std::span<const TermId> args); + + /// Create a variable term. Convenience for makeTerm(var, {}). + TermId makeVar(SymbolId var_symbol); + + /// Look up a term by its ID. + [[nodiscard]] const Term& getTerm(TermId id) const; + + /// Check if a TermId represents a variable (delegates to SymbolTable). + [[nodiscard]] bool isVariable(TermId id) const; + + /// Total number of unique terms stored. + [[nodiscard]] size_t size() const; + + /// Access the underlying SymbolTable. + [[nodiscard]] const SymbolTable& symbols() const { return *symbols_; } + [[nodiscard]] SymbolTable& mutableSymbols() { return *symbols_; } + + private: + struct TermKey { + SymbolId symbol_; + std::vector<TermId> args_; + + bool operator==(const TermKey& other) const = default; + }; + + struct TermKeyHash { + size_t operator()(const TermKey& key) const { + size_t seed = std::hash<uint32_t>{}(key.symbol_); + for (const TermId arg : key.args_) { + seed ^= std::hash<TermId>{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + } + return seed; + } + }; + + SymbolTable* symbols_; + std::vector<Term> terms_; + std::unordered_map<TermKey, TermId, TermKeyHash> term_to_id_; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/core/types.h b/proofsearch/include/atp/core/types.h new file mode 100644 index 0000000..23f2322 --- /dev/null +++ b/proofsearch/include/atp/core/types.h @@ -0,0 +1,79 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file types.h +/// @brief Core type aliases for the ATP engine. + +#include <cstdint> + +namespace atp { + +/// Unique identifier for an interned symbol (predicate/function/constant name). +using SymbolId = uint32_t; + +/// Unique identifier for a term in the Term Bank (hash-consed). +using TermId = uint32_t; + +/// Unique identifier for a clause in the Clause Store. +using ClauseId = uint32_t; + +/// Unique identifier for a sort/type (for sorted logic). +using SortId = uint16_t; + +/// Sentinel value indicating an invalid / unassigned ID. +inline constexpr uint32_t kInvalidId = UINT32_MAX; + +/// Default sort (unsorted logic). +inline constexpr SortId kUnsorted = 0; + +/// Symbol kind — distinguishes variables from function/predicate symbols. +enum class SymbolKind : uint8_t { + kVariable, ///< Universally quantified variable + kConstant, ///< 0-arity function symbol (constant) + kFunction, ///< Function symbol (arity >= 1) + kPredicate, ///< Predicate symbol (returns bool) + kSkolem, ///< Skolem function/constant (introduced by Skolemization) +}; + +/// Inference rule that produced a clause. +/// Deliberately uses uint16_t for extensibility toward algebra/analysis rules. +enum class InferenceRule : uint16_t { + // ── Core resolution rules ── + kInput = 0, ///< Original input clause (axiom / negated conjecture) + kResolution = 1, ///< Binary resolution + kFactoring = 2, ///< Factoring + + // ── Equality rules (algebra) ── + kParamodulation = 100, ///< Paramodulation (equality resolution) + kDemodulation = 101, ///< Demodulation (simplification by rewriting) + kEqualityResolution = 102, ///< s != t resolved with unifier + kEqualityFactoring = 103, ///< Factoring with equality + + // ── Simplification rules ── + kSubsumption = 200, ///< Removed by subsumption + kTautologyElim = 201, ///< Removed as tautology + kPureLiteralElim = 202, ///< Pure literal elimination + + // ── Theory rules (analysis, arithmetic) ── + kTheoryResolution = 300, ///< Theory-specific resolution + kTheoryRewrite = 301, ///< Theory-driven rewriting +}; + +} // namespace atp diff --git a/proofsearch/include/atp/frontend/tptp_parser.h b/proofsearch/include/atp/frontend/tptp_parser.h new file mode 100644 index 0000000..68a5564 --- /dev/null +++ b/proofsearch/include/atp/frontend/tptp_parser.h @@ -0,0 +1,99 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file tptp_parser.h +/// @brief TPTP format parser — converts .p files to internal representations. +/// +/// The parser interns all symbols (predicates, functions, variables) into the +/// SymbolTable and builds terms in the TermBank during parsing. This is the +/// E Prover approach: parse and intern simultaneously, avoiding a separate +/// resolution pass. +/// +/// V1: Hand-written recursive descent for TPTP CNF/FOF subset. +/// (ANTLR4 integration deferred — avoids build complexity for V1.) + +#include "atp/core/clause.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/normalize/formula.h" + +#include <string> +#include <vector> + +namespace atp { + +/// Role of a TPTP formula. +/// See TPTP spec: https://www.tptp.org/TPTP/SyntaxBNF.html +enum class FormulaRole : uint8_t { + kAxiom, ///< Background truth + kHypothesis, ///< Problem-specific assumption + kDefinition, ///< Symbol definition (can be unfolded) + kAssumption, ///< Assumed for this proof attempt + kLemma, ///< Derived intermediate result + kTheorem, ///< Previously proved statement (used as axiom) + kConjecture, ///< The statement to prove + kNegatedConjecture, ///< Already negated conjecture (input was cnf) + kPlain, ///< No semantic role specified +}; + +/// Map a TPTP role string to enum. Returns kPlain for unknown roles. +FormulaRole parseRole(std::string_view role_str); + +/// A parsed TPTP formula with its name and role. +struct AnnotatedFormula { + std::string name_; ///< Formula name (e.g., "axiom1") + FormulaRole role_ = FormulaRole::kPlain; ///< Semantic role + std::unique_ptr<Formula> formula_; ///< The FOL formula (for fof(...)) + std::vector<Clause> clauses_; ///< Direct clauses (for cnf(...)) + bool is_cnf_ = false; ///< true if input was cnf(), false if fof() +}; + +/// A complete parsed TPTP problem. +struct ParsedProblem { + std::vector<AnnotatedFormula> formulas_; + + /// Does any formula contain an equality predicate? + bool has_equality_ = false; + + /// Original file path (for error messages). + std::string source_file_; +}; + +/// Parse a TPTP file. +/// +/// For `cnf(...)` entries: clauses are built directly (no clausification needed). +/// For `fof(...)` entries: Formula AST is built (clausification happens later). +/// +/// All symbols are interned into `symbols` and terms into `bank` during parsing. +ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolTable& symbols); + +/// Parse a TPTP string (for testing). +ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols); + +/// Prepare a parsed problem for proving: +/// 1. Negate conjecture formulas. +/// 2. Clausify all fof() formulas. +/// 3. Collect all cnf() clauses directly. +/// 4. Assign ClauseIds and set provenance to kInput. +/// +/// Returns the final clause set ready for the Prover. +std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank& bank, SymbolTable& symbols); + +} // namespace atp diff --git a/proofsearch/include/atp/index/discrim_tree.h b/proofsearch/include/atp/index/discrim_tree.h new file mode 100644 index 0000000..5f8a206 --- /dev/null +++ b/proofsearch/include/atp/index/discrim_tree.h @@ -0,0 +1,76 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file discrim_tree.h +/// @brief Perfect Discrimination Tree for fast term indexing. +/// +/// Used by subsumption and resolution to quickly find candidate clauses +/// whose literals unify with a query term. Supports three query modes: +/// - Unifiable: find terms that can be unified with the query +/// - Instances: find terms that are instances of the query (more specific) +/// - Generalizations: find terms that are generalizations of the query (more general) + +#include "atp/core/clause.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +#include <vector> + +namespace atp { + +/// A match result from the discrimination tree. +struct IndexMatch { + ClauseId clause_id_; + size_t lit_index_; +}; + +/// A discrimination tree index over terms. +/// Supports insertion and three types of retrieval queries. +class DiscrimTree { + public: + explicit DiscrimTree(const TermBank& bank); + + /// Insert a term (identified by its TermId) with an associated clause/literal ref. + void insert(TermId term, ClauseId clause_id, size_t lit_index); + + /// Retrieve all entries whose indexed term is unifiable with `query`. + [[nodiscard]] std::vector<IndexMatch> queryUnifiable(TermId query) const; + + /// Retrieve all entries whose indexed term is an instance of `query`. + /// (query is more general, indexed term is more specific) + [[nodiscard]] std::vector<IndexMatch> queryInstances(TermId query) const; + + /// Retrieve all entries whose indexed term is a generalization of `query`. + /// (indexed term is more general, query is more specific) + /// This is the key operation for forward subsumption. + [[nodiscard]] std::vector<IndexMatch> queryGeneralizations(TermId query) const; + + /// Remove all entries for a given clause. + void removeClause(ClauseId clause_id); + + /// Number of indexed entries. + [[nodiscard]] size_t size() const; + + private: + const TermBank& bank_; + // TODO: Phase 3 implementation — trie node arena +}; + +} // namespace atp diff --git a/proofsearch/include/atp/infer/resolution.h b/proofsearch/include/atp/infer/resolution.h new file mode 100644 index 0000000..6e2954d --- /dev/null +++ b/proofsearch/include/atp/infer/resolution.h @@ -0,0 +1,50 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file resolution.h +/// @brief Binary resolution and factoring inference rules. + +#include "atp/core/clause.h" +#include "atp/core/term_bank.h" +#include "atp/infer/unification.h" + +#include <optional> +#include <vector> + +namespace atp { + +/// Attempt binary resolution between two clauses on the specified literal indices. +/// @return The resolvent clause if resolution succeeds, std::nullopt otherwise. +std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2, + size_t lit_idx2, const UnificationConfig& uconfig = {}); + +/// Generate all possible resolvents between two clauses. +std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2, + const UnificationConfig& uconfig = {}); + +/// Attempt factoring on a single clause (merge two unifiable literals). +std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig = {}); + +/// Rename all variables in a clause to fresh ones, avoiding conflicts +/// with variables already in the bank. +Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols, + uint32_t& next_var_id); + +} // namespace atp diff --git a/proofsearch/include/atp/infer/substitution.h b/proofsearch/include/atp/infer/substitution.h new file mode 100644 index 0000000..671f6d7 --- /dev/null +++ b/proofsearch/include/atp/infer/substitution.h @@ -0,0 +1,76 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file substitution.h +/// @brief Variable binding map: Var -> Term. +/// +/// Short-lived object created during unification, applied to build resolvents, +/// then discarded. Never stored long-term. + +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +#include <unordered_map> + +namespace atp { + +/// A substitution σ maps variable TermIds to their bound TermIds. +/// +/// Example: σ = { X → f(a), Y → Z } +/// lookup(X) = f(a) (direct binding) +/// resolve(X) = f(a) (same — f(a) is not a variable) +/// resolve(Y) = Z (if Z is unbound, stops at Z) +/// resolve(Y) = f(b) (if Z → f(b) also in σ, walks the chain) +class Substitution { + public: + Substitution() = default; + + /// Bind a variable to a term. Returns false if already bound to a different term. + bool bind(TermId var, TermId term); + + /// Look up what a variable is directly bound to. Returns kInvalidId if unbound. + [[nodiscard]] TermId lookup(TermId var) const; + + /// Walk the binding chain to the final value. + /// If var → Y → f(a), returns f(a). + /// Requires TermBank to check whether intermediate values are variables. + [[nodiscard]] TermId resolve(TermId id, const TermBank& bank) const; + + /// Apply this substitution to a term recursively, creating new terms in the bank. + /// Free (unbound) variables are left as-is. + [[nodiscard]] TermId apply(TermId term, TermBank& bank) const; + + /// Check if a variable occurs anywhere inside a term (for occurs check). + [[nodiscard]] bool occursIn(TermId var, TermId term, const TermBank& bank) const; + + /// Clear all bindings. + void clear(); + + /// Number of bindings. + [[nodiscard]] size_t size() const { return bindings_.size(); } + + /// Check if empty. + [[nodiscard]] bool empty() const { return bindings_.empty(); } + + private: + std::unordered_map<TermId, TermId> bindings_; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/infer/unification.h b/proofsearch/include/atp/infer/unification.h new file mode 100644 index 0000000..870be66 --- /dev/null +++ b/proofsearch/include/atp/infer/unification.h @@ -0,0 +1,43 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file unification.h +/// @brief Most General Unifier (MGU) computation. + +#include "atp/core/term_bank.h" +#include "atp/infer/substitution.h" + +namespace atp { + +/// Configuration for the unification algorithm. +struct UnificationConfig { + bool enable_occurs_check_ = false; ///< Set true for sound but slower unification +}; + +/// Attempt to unify two terms, producing a most general unifier. +/// @return true if unification succeeds, with the MGU in `subst`. +bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, + const UnificationConfig& config = {}); + +/// Apply a substitution to a term recursively, creating new terms in the bank. +/// Free (unbound) variables are left unchanged. +TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank); + +} // namespace atp diff --git a/proofsearch/include/atp/normalize/clausifier.h b/proofsearch/include/atp/normalize/clausifier.h new file mode 100644 index 0000000..61d2505 --- /dev/null +++ b/proofsearch/include/atp/normalize/clausifier.h @@ -0,0 +1,69 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file clausifier.h +/// @brief Converts FOL formulas to Clause Normal Form (CNF). +/// +/// Clausifier is a stateful object because: +/// 1. Skolem function counter must be shared across all formulas in a problem +/// (otherwise different formulas generate conflicting Skolem names). +/// 2. Variable renaming counter must be shared for the same reason. +/// +/// Pipeline: eliminate ↔/→ → NNF → Skolemize → distribute ∨ over ∧ → flatten. + +#include "atp/core/clause.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/normalize/formula.h" + +#include <vector> + +namespace atp { + +/// Stateful clausifier. Create one per proof problem. +/// +/// Usage: +/// Clausifier clausifier(bank, symbols); +/// auto clauses1 = clausifier.clausify(formula1); +/// auto clauses2 = clausifier.clausify(formula2); +/// // Skolem IDs are unique across both calls. +class Clausifier { + public: + Clausifier(TermBank& bank, SymbolTable& symbols); + + /// Convert a single formula to CNF clauses. + /// Skolem functions generated here are globally unique (counter persists). + [[nodiscard]] std::vector<Clause> clausify(const Formula& formula); + + /// Negate a formula: wraps it in ¬(...) + /// Used to negate the conjecture before clausification. + [[nodiscard]] static std::unique_ptr<Formula> negate(std::unique_ptr<Formula> formula); + + /// Number of Skolem functions generated so far. + [[nodiscard]] uint32_t skolemCount() const { return next_skolem_id_; } + + private: + TermBank& bank_; + SymbolTable& symbols_; + uint32_t next_skolem_id_ = 0; + uint32_t next_var_id_ = 0; ///< For variable standardization apart +}; + +} // namespace atp diff --git a/proofsearch/include/atp/normalize/formula.h b/proofsearch/include/atp/normalize/formula.h new file mode 100644 index 0000000..5ee9b94 --- /dev/null +++ b/proofsearch/include/atp/normalize/formula.h @@ -0,0 +1,84 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file formula.h +/// @brief First-order logic formula AST (pre-clausification). +/// +/// Design decision: atoms use TermId (interned), quantifier variables use +/// SymbolId (interned). The parser interns all symbols during parsing. +/// This avoids string→ID lookups during clausification and ensures +/// consistent variable identity across quantifier scopes. + +#include "atp/core/types.h" + +#include <memory> +#include <vector> + +namespace atp { + +/// AST node types for first-order logic formulas. +enum class FormulaKind : uint8_t { + kAtom, ///< Predicate application: P(t1, ..., tn) + kEquality, ///< Equality atom: t1 = t2 (distinguished for equality reasoning) + kNot, ///< Negation: ¬F + kAnd, ///< Conjunction: F ∧ G + kOr, ///< Disjunction: F ∨ G + kImplies, ///< Implication: F → G + kIff, ///< Biconditional: F ↔ G + kForall, ///< Universal: ∀x. F + kExists, ///< Existential: ∃x. F +}; + +/// A first-order logic formula node. +/// +/// All identifiers are interned: atoms as TermIds, quantifier variables as +/// SymbolIds. No raw strings survive past the parser. +struct Formula { + FormulaKind kind_; + + /// For kAtom / kEquality: the predicate/equality term, already interned. + TermId atom_ = kInvalidId; + + /// For kForall / kExists: the bound variable, as an interned SymbolId. + /// Using SymbolId (not string) so the clausifier can map bound variables + /// back to term-bank variables without string lookups. + SymbolId bound_var_ = kInvalidId; + + /// Sub-formulas (1 for Not/Quantifiers, 2 for binary connectives). + std::vector<std::unique_ptr<Formula>> children_; + + // ── Factory methods ── + + static std::unique_ptr<Formula> makeAtom(TermId atom); + static std::unique_ptr<Formula> makeEquality(TermId lhs, TermId rhs, TermId eq_atom); + static std::unique_ptr<Formula> makeNot(std::unique_ptr<Formula> child); + static std::unique_ptr<Formula> makeAnd(std::unique_ptr<Formula> lhs, + std::unique_ptr<Formula> rhs); + static std::unique_ptr<Formula> makeOr(std::unique_ptr<Formula> lhs, + std::unique_ptr<Formula> rhs); + static std::unique_ptr<Formula> makeImplies(std::unique_ptr<Formula> lhs, + std::unique_ptr<Formula> rhs); + static std::unique_ptr<Formula> makeIff(std::unique_ptr<Formula> lhs, + std::unique_ptr<Formula> rhs); + static std::unique_ptr<Formula> makeForall(SymbolId var, std::unique_ptr<Formula> body); + static std::unique_ptr<Formula> makeExists(SymbolId var, std::unique_ptr<Formula> body); +}; + +} // namespace atp diff --git a/proofsearch/include/atp/proof/proof_trace.h b/proofsearch/include/atp/proof/proof_trace.h new file mode 100644 index 0000000..4ea7aa1 --- /dev/null +++ b/proofsearch/include/atp/proof/proof_trace.h @@ -0,0 +1,55 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file proof_trace.h +/// @brief Proof reconstruction from the empty clause back to axioms. + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/term_bank.h" + +#include <string> +#include <vector> + +namespace atp { + +/// A single step in a reconstructed proof. +struct ProofStep { + ClauseId clause_id_; + InferenceRule rule_; + ClauseId parent1_; + ClauseId parent2_; +}; + +/// Reconstruct the proof trace from the empty clause. +/// Returns steps in topological order: axioms first, empty clause last. +std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_clause_id); + +/// Convert a TermId back to a human-readable string. +std::string termToString(TermId id, const TermBank& bank); + +/// Convert a Clause to a human-readable string. +std::string clauseToString(const Clause& clause, const TermBank& bank); + +/// Format a proof as a human-readable string. +std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore& store, + const TermBank& bank); + +} // namespace atp diff --git a/proofsearch/include/atp/rewrite/ordering.h b/proofsearch/include/atp/rewrite/ordering.h new file mode 100644 index 0000000..195c3c6 --- /dev/null +++ b/proofsearch/include/atp/rewrite/ordering.h @@ -0,0 +1,52 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file ordering.h +/// @brief Term orderings for equality reasoning (KBO, LPO). +/// +/// Term orderings are the foundation of equality-based theorem proving. +/// They ensure that rewriting always terminates by enforcing a well-founded +/// ordering on terms. Required by paramodulation, demodulation, and +/// ordered resolution. + +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +namespace atp { + +/// Ordering comparison result. +enum class OrderResult : uint8_t { + kLessThan, ///< t1 < t2 + kEqual, ///< t1 = t2 + kGreaterThan, ///< t1 > t2 + kIncomparable, ///< t1 and t2 are incomparable +}; + +/// Abstract base for term orderings. +/// Concrete implementations: KBO (Knuth-Bendix), LPO (Lexicographic Path). +class TermOrdering { + public: + virtual ~TermOrdering() = default; + + /// Compare two terms under the ordering. + [[nodiscard]] virtual OrderResult compare(const TermBank& bank, TermId t1, TermId t2) const = 0; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/rewrite/paramodulation.h b/proofsearch/include/atp/rewrite/paramodulation.h new file mode 100644 index 0000000..9dfbd66 --- /dev/null +++ b/proofsearch/include/atp/rewrite/paramodulation.h @@ -0,0 +1,47 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file paramodulation.h +/// @brief Paramodulation inference rule for equality reasoning. +/// +/// Paramodulation replaces a subterm in one clause with an equal term +/// from an equation in another clause. Combined with term orderings, +/// this gives a complete calculus for first-order logic with equality +/// (the Superposition calculus). + +#include "atp/core/clause.h" +#include "atp/core/term_bank.h" +#include "atp/rewrite/ordering.h" + +#include <vector> + +namespace atp { + +/// Generate all paramodulants between two clauses. +/// Uses the term ordering to restrict to ordered paramodulation (superposition). +std::vector<Clause> paramodulate(const TermBank& bank, const Clause& c1, const Clause& c2, + const TermOrdering& ordering); + +/// Simplify a clause by demodulation (rewriting with unit equalities). +/// Returns true if the clause was modified. +bool demodulate(TermBank& bank, Clause& clause, const Clause& unit_eq, + const TermOrdering& ordering); + +} // namespace atp diff --git a/proofsearch/include/atp/search/clause_queue.h b/proofsearch/include/atp/search/clause_queue.h new file mode 100644 index 0000000..dfb575c --- /dev/null +++ b/proofsearch/include/atp/search/clause_queue.h @@ -0,0 +1,43 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file clause_queue.h +/// @brief Priority queue for the Given Clause Loop. + +#include "atp/core/clause.h" + +#include <functional> + +namespace atp { + +/// Comparison function type for clause ordering. +using ClauseComparator = std::function<bool(const Clause& a, const Clause& b)>; + +/// BFS comparator: prioritize shallower derivation depth. +inline bool bfsCompare(const Clause& a, const Clause& b) { + return a.depth_ > b.depth_; // min-heap by depth +} + +/// Weight comparator: prioritize shorter (fewer literals) clauses. +inline bool weightCompare(const Clause& a, const Clause& b) { + return a.literals_.size() > b.literals_.size(); // min-heap by literal count +} + +} // namespace atp diff --git a/proofsearch/include/atp/search/prover.h b/proofsearch/include/atp/search/prover.h new file mode 100644 index 0000000..65ec7f0 --- /dev/null +++ b/proofsearch/include/atp/search/prover.h @@ -0,0 +1,92 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file prover.h +/// @brief The Given Clause Loop — main saturation-based proof search. +/// +/// V1: Uses a simple ProverConfig with hardcoded resolution + factoring. +/// V2: Will be refactored to accept a Calculus object from strategy/ module +/// for dynamic algorithm loading per problem type. + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/term_bank.h" +#include "atp/search/clause_queue.h" + +#include <optional> +#include <queue> +#include <vector> + +namespace atp { + +/// Result of a proof attempt. +enum class ProverResult : uint8_t { + kTheorem, ///< Empty clause derived — conjecture is a theorem + kSaturation, ///< Search space saturated — cannot prove + kTimeout, ///< Resource limit exceeded +}; + +/// V1 configuration — simple and direct. +/// Future: replaced by strategy::Calculus for dynamic rule loading. +struct ProverConfig { + ClauseComparator comparator_ = bfsCompare; + size_t max_clauses_ = 100000; ///< Safety limit + size_t max_iterations_ = 500000; ///< Safety limit + bool enable_occurs_check_ = false; +}; + +/// Main prover class implementing the Given Clause Loop. +/// V1: hardcodes resolution + factoring + subsumption. +/// V2: will accept a Calculus object for pluggable inference rules. +class Prover { + public: + Prover(TermBank& bank, ClauseStore& store, ProverConfig config = {}); + + /// Add initial clauses (axioms + negated conjecture). + void addClauses(std::vector<Clause> clauses); + + /// Run the proof search. + ProverResult prove(); + + /// After a successful proof, retrieve the empty clause ID. + [[nodiscard]] std::optional<ClauseId> getEmptyClauseId() const; + + /// Access the underlying clause store. + [[nodiscard]] const ClauseStore& clauseStore() const { return store_; } + + private: + [[nodiscard]] bool hitResourceLimit(size_t iterations) const; + [[nodiscard]] Clause popGivenClause(); + [[nodiscard]] bool isForwardSubsumedByProcessed(const Clause& clause) const; + [[nodiscard]] bool shouldSkipGiven(const Clause& given) const; + void applyBackwardSubsumption(const Clause& given); + [[nodiscard]] std::vector<Clause> generateNewClauses(const Clause& given) const; + [[nodiscard]] uint16_t computeDepth(const Clause& clause) const; + [[nodiscard]] std::optional<ClauseId> processNewClauses(std::vector<Clause> new_clauses); + + TermBank& bank_; + ClauseStore& store_; + ProverConfig config_; + std::priority_queue<Clause, std::vector<Clause>, ClauseComparator> unprocessed_; + std::vector<ClauseId> processed_; + std::optional<ClauseId> empty_clause_id_; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/simplify/subsumption.h b/proofsearch/include/atp/simplify/subsumption.h new file mode 100644 index 0000000..970b6d8 --- /dev/null +++ b/proofsearch/include/atp/simplify/subsumption.h @@ -0,0 +1,56 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file subsumption.h +/// @brief Forward and backward subsumption checks (backed by discrimination tree). + +#include "atp/core/clause.h" +#include "atp/index/discrim_tree.h" + +#include <vector> + +namespace atp { + +/// Subsumption engine: checks if a new clause is subsumed by existing ones +/// (forward) or subsumes existing ones (backward). +class SubsumptionEngine { + public: + explicit SubsumptionEngine(const TermBank& bank); + + /// Returns true if `candidate` is subsumed by any existing clause. + [[nodiscard]] bool isForwardSubsumed(const Clause& candidate) const; + + /// Returns IDs of existing clauses that are subsumed by `new_clause`. + [[nodiscard]] std::vector<ClauseId> backwardSubsumed(const Clause& new_clause) const; + + /// Add a clause to the subsumption index. + void addClause(const Clause& clause); + + /// Remove a clause from the subsumption index. + void removeClause(ClauseId id); + + private: + DiscrimTree index_; + // TODO: Phase 5 implementation +}; + +bool subsumes(const Clause& general, const Clause& specific); + +} // namespace atp diff --git a/proofsearch/include/atp/simplify/tautology.h b/proofsearch/include/atp/simplify/tautology.h new file mode 100644 index 0000000..f17f0c7 --- /dev/null +++ b/proofsearch/include/atp/simplify/tautology.h @@ -0,0 +1,31 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file tautology.h +/// @brief Tautology detection for clauses. + +#include "atp/core/clause.h" + +namespace atp { + +/// Returns true if the clause is a tautology (contains complementary literals). +[[nodiscard]] bool isTautology(const Clause& clause); + +} // namespace atp diff --git a/proofsearch/include/atp/strategy/calculus.h b/proofsearch/include/atp/strategy/calculus.h new file mode 100644 index 0000000..e06988e --- /dev/null +++ b/proofsearch/include/atp/strategy/calculus.h @@ -0,0 +1,67 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file calculus.h +/// @brief A Calculus bundles the exact set of inference rules + heuristics +/// to use for a specific problem class. +/// +/// Think of it as the "algorithm profile" that the Prover loads. +/// Different problems get different calculi: +/// - Pure propositional: resolution + factoring only +/// - FOL without equality: + full unification +/// - FOL with equality: + paramodulation + KBO ordering +/// - Arithmetic: + theory solver integration +/// +/// This is the single point where search space control happens. + +#include "atp/rewrite/ordering.h" +#include "atp/search/clause_queue.h" +#include "atp/strategy/inference_rule.h" + +#include <memory> +#include <string_view> +#include <vector> + +namespace atp { + +/// A Calculus = a complete specification of how to search for a proof. +/// The Prover is parameterized by this — it never hardcodes which rules to use. +struct Calculus { + /// Name for logging (e.g., "superposition", "pure_resolution"). + std::string name; + + /// Generating rules (executed in order during the main loop). + std::vector<std::unique_ptr<GeneratingRule>> generating_rules; + + /// Simplifying rules (applied to each new clause before enqueuing). + std::vector<std::unique_ptr<SimplifyingRule>> simplifying_rules; + + /// Clause selection heuristic. + ClauseComparator comparator = bfsCompare; + + /// Term ordering (nullptr if equality reasoning is disabled). + std::unique_ptr<TermOrdering> ordering = nullptr; + + /// Resource limits. + size_t max_clauses = 100000; + size_t max_iterations = 500000; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/strategy/inference_rule.h b/proofsearch/include/atp/strategy/inference_rule.h new file mode 100644 index 0000000..88b6fe0 --- /dev/null +++ b/proofsearch/include/atp/strategy/inference_rule.h @@ -0,0 +1,80 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file inference_rule.h +/// @brief Abstract interface for pluggable inference rules. +/// +/// Each inference rule (resolution, factoring, paramodulation, etc.) +/// is a self-contained object that the Prover can selectively load. +/// This prevents search space explosion by only enabling rules relevant +/// to the problem at hand. + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/term_bank.h" + +#include <string_view> +#include <vector> + +namespace atp { + +/// Abstract base class for all inference rules. +/// The Prover invokes only the rules present in its active calculus. +class InferenceRuleBase { + public: + virtual ~InferenceRuleBase() = default; + + /// Human-readable name for logging and proof output. + [[nodiscard]] virtual std::string_view name() const = 0; + + /// Is this a generating rule (produces new clauses) or simplifying rule + /// (rewrites/deletes existing clauses)? + enum class Kind : uint8_t { kGenerating, kSimplifying }; + [[nodiscard]] virtual Kind kind() const = 0; +}; + +/// Generating inference rule: given a "given clause" and the set of processed +/// clauses, produce new clauses. +class GeneratingRule : public InferenceRuleBase { + public: + [[nodiscard]] Kind kind() const final { return Kind::kGenerating; } + + /// Generate new clauses from the given clause against all processed clauses. + /// @param given The selected clause from the Unprocessed queue. + /// @param processed All previously processed clauses (accessed via store). + /// @param bank The global term bank. + /// @return Newly generated clauses (not yet added to the store). + [[nodiscard]] virtual std::vector<Clause> generate(const Clause& given, + const std::vector<ClauseId>& processed, + const ClauseStore& store, + TermBank& bank) const = 0; +}; + +/// Simplifying inference rule: rewrite or delete a clause in-place. +class SimplifyingRule : public InferenceRuleBase { + public: + [[nodiscard]] Kind kind() const final { return Kind::kSimplifying; } + + /// Attempt to simplify a clause. Returns true if the clause was modified. + /// If the clause should be deleted entirely, clear its literals. + virtual bool simplify(Clause& clause, const ClauseStore& store, TermBank& bank) const = 0; +}; + +} // namespace atp diff --git a/proofsearch/include/atp/strategy/problem_analyzer.h b/proofsearch/include/atp/strategy/problem_analyzer.h new file mode 100644 index 0000000..5e6c5cf --- /dev/null +++ b/proofsearch/include/atp/strategy/problem_analyzer.h @@ -0,0 +1,61 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file problem_analyzer.h +/// @brief Analyzes input clauses and selects the optimal Calculus. +/// +/// Before the Prover starts its main loop, the ProblemAnalyzer inspects +/// the input clause set to determine problem characteristics: +/// - Contains equality? → enable paramodulation +/// - Pure Horn clauses? → use SLD resolution +/// - Contains arithmetic literals? → enable theory solver +/// - Problem size / clause density → tune resource limits +/// +/// This is the "auto mode" that mature ATPs use to avoid loading +/// unnecessary inference rules that would explode the search space. + +#include "atp/core/clause.h" +#include "atp/strategy/calculus.h" + +#include <vector> + +namespace atp { + +/// Features detected in the input problem. +struct ProblemFeatures { + bool has_equality = false; ///< Contains '=' predicate + bool is_purely_propositional = false; ///< No function symbols, no variables + bool is_horn = false; ///< All clauses are Horn clauses + bool has_existential = false; ///< Had existential quantifiers (Skolemized) + size_t num_clauses = 0; + size_t num_predicates = 0; + size_t num_functions = 0; + size_t max_clause_size = 0; + size_t max_term_depth = 0; +}; + +/// Analyze the input clauses and extract problem features. +ProblemFeatures analyzeFeatures(const std::vector<Clause>& clauses, const TermBank& bank); + +/// Select the optimal calculus based on detected features. +/// This is the core strategy dispatch logic. +std::unique_ptr<Calculus> selectCalculus(const ProblemFeatures& features); + +} // namespace atp diff --git a/proofsearch/include/atp/utils/hash_utils.h b/proofsearch/include/atp/utils/hash_utils.h new file mode 100644 index 0000000..ae31f43 --- /dev/null +++ b/proofsearch/include/atp/utils/hash_utils.h @@ -0,0 +1,46 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file hash_utils.h +/// @brief Hash combination utilities. + +#include <cstddef> +#include <cstdint> +#include <functional> + +namespace atp { + +/// Combine a hash with a new value (boost::hash_combine style). +inline void hashCombine(size_t& seed, size_t value) { + seed ^= value + 0x9e3779b9 + (seed << 6) + (seed >> 2); +} + +/// Hash a span of values. +template <typename T> +size_t hashRange(const T* data, size_t count) { + size_t seed = 0; + std::hash<T> hasher; + for (size_t i = 0; i < count; ++i) { + hashCombine(seed, hasher(data[i])); + } + return seed; +} + +} // namespace atp diff --git a/proofsearch/include/atp/utils/logger.h b/proofsearch/include/atp/utils/logger.h new file mode 100644 index 0000000..de77c54 --- /dev/null +++ b/proofsearch/include/atp/utils/logger.h @@ -0,0 +1,41 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#pragma once + +/// @file logger.h +/// @brief Minimal high-performance logging macros. + +#include <cstdio> + +#ifndef ATP_LOG_LEVEL +#define ATP_LOG_LEVEL 2 // 0=TRACE, 1=DEBUG, 2=INFO, 3=WARN, 4=ERROR +#endif + +#define ATP_LOG(level, level_str, fmt, ...) \ + do { \ + if constexpr (level >= ATP_LOG_LEVEL) { \ + std::fprintf(stderr, "[%s] " fmt "\n", level_str, ##__VA_ARGS__); \ + } \ + } while (0) + +#define ATP_TRACE(fmt, ...) ATP_LOG(0, "TRACE", fmt, ##__VA_ARGS__) +#define ATP_DEBUG(fmt, ...) ATP_LOG(1, "DEBUG", fmt, ##__VA_ARGS__) +#define ATP_INFO(fmt, ...) ATP_LOG(2, "INFO", fmt, ##__VA_ARGS__) +#define ATP_WARN(fmt, ...) ATP_LOG(3, "WARN", fmt, ##__VA_ARGS__) +#define ATP_ERROR(fmt, ...) ATP_LOG(4, "ERROR", fmt, ##__VA_ARGS__) diff --git a/proofsearch/src/core/clause_store.cc b/proofsearch/src/core/clause_store.cc new file mode 100644 index 0000000..f8ee73d --- /dev/null +++ b/proofsearch/src/core/clause_store.cc @@ -0,0 +1,59 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/clause_store.h" + +#include "atp/core/clause.h" +#include "atp/core/types.h" + +#include <cassert> +#include <cstddef> +#include <functional> +#include <utility> + +namespace atp { + +ClauseId ClauseStore::addClause(Clause clause) { + auto new_id = static_cast<ClauseId>(clauses_.size()); + clause.id_ = new_id; + clauses_.push_back(std::move(clause)); + return new_id; +} + +const Clause& ClauseStore::getClause(ClauseId id) const { + assert(id < clauses_.size() && "ClauseId out of bounds!"); + return clauses_[id]; +} + +Clause& ClauseStore::getMutableClause(ClauseId id) { + assert(id < clauses_.size() && "ClauseId out of bounds!"); + return clauses_[id]; +} + +size_t ClauseStore::size() const { + return clauses_.size(); +} + +void ClauseStore::forEach(const std::function<void(const Clause&)>& visitor) const { + for (const auto& clause : clauses_) { + // TODO: Tombstone mechanism + visitor(clause); + } +} + +} // namespace atp diff --git a/proofsearch/src/core/symbol_table.cc b/proofsearch/src/core/symbol_table.cc new file mode 100644 index 0000000..b707132 --- /dev/null +++ b/proofsearch/src/core/symbol_table.cc @@ -0,0 +1,65 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/symbol_table.h" + +#include "atp/core/types.h" + +#include <cstddef> +#include <cstdint> +#include <stdexcept> +#include <string> +#include <string_view> + +namespace atp { + +SymbolId SymbolTable::intern(std::string_view name, SymbolKind kind, uint16_t arity, SortId sort) { + auto it = name_to_id_.find(name); + if (it != name_to_id_.end()) { + SymbolId const id = it->second; + SymbolInfo const& info = infos_[id]; + if (info.kind_ != kind || info.arity_ != arity) { + throw std::runtime_error("Symbol kind or arity mismatch for: " + std::string(name)); + } + return id; + } + auto new_id = static_cast<SymbolId>(infos_.size()); + infos_.push_back(SymbolInfo{ + .name_ = std::string(name), .kind_ = kind, .arity_ = arity, .sort_ = sort}); + std::string_view const stable_name_view = infos_.back().name_; + name_to_id_.emplace(stable_name_view, new_id); + return new_id; +} + +std::string_view SymbolTable::getName(SymbolId id) const { + return infos_[id].name_; +} + +const SymbolInfo& SymbolTable::getInfo(SymbolId id) const { + return infos_[id]; +} + +bool SymbolTable::isVariable(SymbolId id) const { + return infos_[id].kind_ == SymbolKind::kVariable; +} + +size_t SymbolTable::size() const { + return infos_.size(); +} + +} // namespace atp diff --git a/proofsearch/src/core/term_bank.cc b/proofsearch/src/core/term_bank.cc new file mode 100644 index 0000000..0dc166f --- /dev/null +++ b/proofsearch/src/core/term_bank.cc @@ -0,0 +1,63 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/term_bank.h" + +#include "atp/core/term.h" +#include "atp/core/types.h" + +#include <cassert> +#include <cstddef> +#include <span> +#include <utility> +#include <vector> + +namespace atp { + +TermId TermBank::makeTerm(SymbolId symbol, std::span<const TermId> args) { + TermKey key{.symbol_ = symbol, .args_ = {args.begin(), args.end()}}; + auto it = term_to_id_.find(key); + if (it != term_to_id_.end()) { + return it->second; + } + auto new_id = static_cast<TermId>(terms_.size()); + Term new_term{.symbol_id_ = symbol, .args_ = key.args_}; + terms_.push_back(std::move(new_term)); + term_to_id_.emplace(std::move(key), new_id); + return new_id; +} + +TermId TermBank::makeVar(SymbolId var_symbol) { + return makeTerm(var_symbol, {}); +} + +const Term& TermBank::getTerm(TermId id) const { + assert(id < terms_.size() && "TermId out of bounds!"); + return terms_[id]; +} + +bool TermBank::isVariable(TermId id) const { + assert(id < terms_.size() && "TermId out of bounds!"); + return symbols_->isVariable(terms_[id].symbol_id_); +} + +size_t TermBank::size() const { + return terms_.size(); +} + +} // namespace atp diff --git a/proofsearch/src/frontend/tptp_parser.cc b/proofsearch/src/frontend/tptp_parser.cc new file mode 100644 index 0000000..10190b8 --- /dev/null +++ b/proofsearch/src/frontend/tptp_parser.cc @@ -0,0 +1,325 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/frontend/tptp_parser.h" + +#include "atp/core/clause.h" +#include "atp/core/literal.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +#include <cctype> +#include <cstddef> +#include <cstdint> +#include <fstream> +#include <ios> +#include <iterator> +#include <stdexcept> +#include <string> +#include <string_view> +#include <unordered_map> +#include <utility> +#include <vector> + +namespace atp { + +FormulaRole parseRole(std::string_view role_str) { + if (role_str == "axiom") { + return FormulaRole::kAxiom; + } + if (role_str == "hypothesis") { + return FormulaRole::kHypothesis; + } + if (role_str == "definition") { + return FormulaRole::kDefinition; + } + if (role_str == "assumption") { + return FormulaRole::kAssumption; + } + if (role_str == "lemma") { + return FormulaRole::kLemma; + } + if (role_str == "theorem") { + return FormulaRole::kTheorem; + } + if (role_str == "conjecture") { + return FormulaRole::kConjecture; + } + if (role_str == "negated_conjecture") { + return FormulaRole::kNegatedConjecture; + } + if (role_str == "plain") { + return FormulaRole::kPlain; + } + return FormulaRole::kPlain; +} + +enum class TokenType : std::uint8_t { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown }; + +struct Token { + TokenType type_{}; + std::string_view value_; + size_t line_{}; + size_t column_{}; +}; + +class TptpLexer { + public: + explicit TptpLexer(std::string_view input) : source_(input) {} + + Token nextToken() { + skipWhitespaceAndComments(); + + if (pos_ >= source_.length()) { + return {.type_ = TokenType::kEOF, .value_ = "", .line_ = line_, .column_ = column_}; + } + + size_t const start_pos = pos_; + [[maybe_unused]] size_t const start_col = column_; + char const c = source_[pos_]; + + if ((std::isalpha(static_cast<unsigned char>(c)) != 0) || c == '_') { + while ( + pos_ < source_.size() && + ((std::isalnum(static_cast<unsigned char>(source_[pos_])) != 0) || source_[pos_] == '_')) { + advanceChar(); + } + return {.type_ = TokenType::kWord, + .value_ = source_.substr(start_pos, pos_ - start_pos), + .line_ = line_, + .column_ = column_}; + } + + advanceChar(); + switch (c) { + case '(': + return {.type_ = TokenType::kLParen, .value_ = "(", .line_ = line_, .column_ = column_}; + case ')': + return {.type_ = TokenType::kRParen, .value_ = ")", .line_ = line_, .column_ = column_}; + case ',': + return {.type_ = TokenType::kComma, .value_ = ",", .line_ = line_, .column_ = column_}; + case '.': + return {.type_ = TokenType::kDot, .value_ = ".", .line_ = line_, .column_ = column_}; + case '~': + return {.type_ = TokenType::kNot, .value_ = "~", .line_ = line_, .column_ = column_}; + case '|': + return {.type_ = TokenType::kOr, .value_ = "|", .line_ = line_, .column_ = column_}; + default: + return {.type_ = TokenType::kUnkown, + .value_ = source_.substr(start_pos, 1), + .line_ = line_, + .column_ = column_}; + } + } + + private: + std::string_view source_; + size_t pos_ = 0; + size_t line_ = 1; + size_t column_ = 1; + + void advanceChar() { + if (pos_ < source_.size()) { + if (source_[pos_] == '\n') { + line_++; + column_ = 1; + } else { + column_++; + } + pos_++; + } + } + + void skipWhitespaceAndComments() { + while (pos_ < source_.size()) { + char const c = source_[pos_]; + if (std::isspace(static_cast<unsigned char>(c)) != 0) { + advanceChar(); + } else if (c == '%') { + while (pos_ < source_.size() && source_[pos_] != '\n') { + advanceChar(); + } + } else { + break; + } + } + } +}; + +class TptpParser { + public: + explicit TptpParser(std::string_view input, TermBank& bank, SymbolTable& symbols) + : lexer_(input), bank_(bank), symbols_(symbols) { + advance(); + } + + void parseProblem(ParsedProblem& problem) { + while (current_token_.type_ != TokenType::kEOF) { + if (current_token_.type_ == TokenType::kWord && current_token_.value_ == "cnf") { + advance(); + expect(TokenType::kLParen); + + AnnotatedFormula af; + af.is_cnf_ = true; + + af.name_ = std::string(current_token_.value_); + expect(TokenType::kWord); + expect(TokenType::kComma); + + af.role_ = parseRole(current_token_.value_); + expect(TokenType::kWord); + expect(TokenType::kComma); + + Clause clause; + clause.literals_.push_back(parseLiteral()); + while (current_token_.type_ == TokenType::kOr) { + advance(); + clause.literals_.push_back(parseLiteral()); + } + af.clauses_.push_back(std::move(clause)); + + expect(TokenType::kRParen); + expect(TokenType::kDot); + problem.formulas_.push_back(std::move(af)); + + variable_cache_.clear(); + } else if (current_token_.value_ == "fof") { + throw std::runtime_error("FOF parsing not implemented. Line " + + std::to_string(current_token_.line_)); + } else { + throw std::runtime_error("Unknown declaration: '" + + std::string(current_token_.value_) + "'"); + } + } + } + + private: + TptpLexer lexer_; + TermBank& bank_; + SymbolTable& symbols_; + Token current_token_{}; + std::vector<Token> tokens_; + std::unordered_map<std::string_view, SymbolId> variable_cache_; + + void advance() { current_token_ = lexer_.nextToken(); } + + void expect(TokenType type) { + if (current_token_.type_ != type) { + throw std::runtime_error("Parse error at line " + std::to_string(current_token_.line_) + + ", col " + std::to_string(current_token_.column_) + + ": unexpected token '" + std::string(current_token_.value_) + + "'"); + } + advance(); + } + + TermId parseTerm() { + if (current_token_.type_ != TokenType::kWord) { + throw std::runtime_error("Expected variable or function name at line " + + std::to_string(current_token_.line_) + ", col " + + std::to_string(current_token_.column_) + + ": unexpected token '" + std::string(current_token_.value_) + + "'"); + } + + std::string_view const name = current_token_.value_; + bool const is_variable = std::isupper(static_cast<unsigned char>(name[0])) != 0; + advance(); + + if (is_variable) { + // Check cache first — same variable name in one clause → same TermId + auto it = variable_cache_.find(name); + if (it != variable_cache_.end()) { + return it->second; + } + SymbolId const sym = symbols_.intern(name, SymbolKind::kVariable); + TermId const var_id = bank_.makeVar(sym); + variable_cache_[name] = var_id; + return var_id; + } + + // Check if this is a function/predicate (has args) or a constant (no parens) + if (current_token_.type_ == TokenType::kLParen) { + advance(); // consume '(' + std::vector<TermId> args; + if (current_token_.type_ != TokenType::kRParen) { + args.push_back(parseTerm()); + while (current_token_.type_ == TokenType::kComma) { + advance(); + args.push_back(parseTerm()); + } + } + expect(TokenType::kRParen); + const SymbolId sym = symbols_.intern(name, SymbolKind::kFunction, + static_cast<uint16_t>(args.size())); + return bank_.makeTerm(sym, args); + } + + // Constant: no parentheses (e.g., a, b, h0, s0) + const SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0); + return bank_.makeTerm(sym, {}); + } + + Literal parseLiteral() { + bool is_positive = true; + if (current_token_.type_ == TokenType::kNot) { + is_positive = false; + advance(); + } + TermId const term = parseTerm(); + return Literal{.atom_ = term, .is_positive_ = is_positive}; + } +}; + +ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols) { + ParsedProblem problem; + TptpParser parser(input, bank, symbols); + parser.parseProblem(problem); + return problem; +} + +ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolTable& symbols) { + std::ifstream file(filename, std::ios::binary); + if (!file.is_open()) { + throw std::runtime_error("Failed to open file: " + filename); + } + std::string const content((std::istreambuf_iterator<char>(file)), std::istreambuf_iterator<char>()); + ParsedProblem problem = parseTptpString(content, bank, symbols); + problem.source_file_ = filename; + return problem; +} + +std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank& /*bank*/, + SymbolTable& /*symbols*/) { + std::vector<Clause> final_clauses; + + for (auto& af : problem.formulas_) { + if (af.is_cnf_) { + for (auto& clause : af.clauses_) { + clause.rule_ = InferenceRule::kInput; + clause.parent1_ = kInvalidId; + clause.parent2_ = kInvalidId; + final_clauses.push_back(std::move(clause)); + } + } + } + return final_clauses; +} + +} // namespace atp diff --git a/proofsearch/src/index/discrim_tree.cc b/proofsearch/src/index/discrim_tree.cc new file mode 100644 index 0000000..17c63f8 --- /dev/null +++ b/proofsearch/src/index/discrim_tree.cc @@ -0,0 +1,17 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ diff --git a/proofsearch/src/infer/resolution.cc b/proofsearch/src/infer/resolution.cc new file mode 100644 index 0000000..5fb0d4a --- /dev/null +++ b/proofsearch/src/infer/resolution.cc @@ -0,0 +1,176 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/infer/resolution.h" + +#include "atp/core/clause.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/infer/substitution.h" +#include "atp/infer/unification.h" + +#include <cstddef> +#include <cstdint> +#include <optional> +#include <string> +#include <unordered_map> +#include <utility> +#include <vector> + +namespace atp { + +namespace { + +/// Recursively collect all variable TermIds appearing in a term. +void collectVariables(TermId term, const TermBank& bank, std::unordered_map<TermId, bool>& seen) { + if (bank.isVariable(term)) { + seen[term] = true; + return; + } + // Copy args to avoid dangling ref (bank is const here, but be safe) + const Term& t = bank.getTerm(term); + for (TermId const arg : t.args_) { + collectVariables(arg, bank, seen); + } +} + +} // namespace + +Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols, + uint32_t& next_var_id) { + // 1. Collect all variables in the clause + std::unordered_map<TermId, bool> var_set; + for (const auto& lit : c.literals_) { + collectVariables(lit.atom_, bank, var_set); + } + + if (var_set.empty()) { + return c; // Ground clause — nothing to rename + } + + // 2. Create fresh variables and build a substitution + Substitution rename_subst; + for (auto& [old_var_id, _] : var_set) { + std::string const fresh_name = "_R" + std::to_string(next_var_id++); + SymbolId const fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable); + TermId const fresh_var = bank.makeVar(fresh_sym); + rename_subst.bind(old_var_id, fresh_var); + } + + // 3. Apply the renaming substitution to all literals + Clause renamed; + renamed.id_ = c.id_; + renamed.rule_ = c.rule_; + renamed.parent1_ = c.parent1_; + renamed.parent2_ = c.parent2_; + renamed.depth_ = c.depth_; + for (const auto& lit : c.literals_) { + TermId const new_atom = applySubstitution(rename_subst, lit.atom_, bank); + renamed.literals_.push_back({.atom_ = new_atom, .is_positive_ = lit.is_positive_}); + } + return renamed; +} + +std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2, + size_t lit_idx2, const UnificationConfig& uconfig) { + // Must have opposite polarity + if (c1.literals_[lit_idx1].is_positive_ == c2.literals_[lit_idx2].is_positive_) { + return std::nullopt; + } + + // Rename c2's variables to avoid clashes with c1 + // Use a static counter — safe for single-threaded prover + static uint32_t var_counter = 0; + auto& symbols = bank.mutableSymbols(); + Clause c2r = renameVariables(c2, bank, symbols, var_counter); + + // Unify the complementary atoms + Substitution subst; + if (!unify(bank, c1.literals_[lit_idx1].atom_, c2r.literals_[lit_idx2].atom_, subst, uconfig)) { + return std::nullopt; + } + + // Build the resolvent: all literals except the resolved pair, with subst applied + Clause resolvent; + resolvent.rule_ = InferenceRule::kResolution; + resolvent.parent1_ = c1.id_; + resolvent.parent2_ = c2.id_; + + for (size_t i = 0; i < c1.literals_.size(); ++i) { + if (i != lit_idx1) { + TermId const new_atom = applySubstitution(subst, c1.literals_[i].atom_, bank); + resolvent.literals_.push_back( + {.atom_ = new_atom, .is_positive_ = c1.literals_[i].is_positive_}); + } + } + for (size_t i = 0; i < c2r.literals_.size(); ++i) { + if (i != lit_idx2) { + TermId const new_atom = applySubstitution(subst, c2r.literals_[i].atom_, bank); + resolvent.literals_.push_back( + {.atom_ = new_atom, .is_positive_ = c2r.literals_[i].is_positive_}); + } + } + return resolvent; +} + +std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2, + const UnificationConfig& uconfig) { + std::vector<Clause> results; + for (size_t i = 0; i < c1.literals_.size(); ++i) { + for (size_t j = 0; j < c2.literals_.size(); ++j) { + if (c1.literals_[i].is_positive_ != c2.literals_[j].is_positive_) { + if (auto r = resolve(bank, c1, i, c2, j, uconfig)) { + results.push_back(std::move(*r)); + } + } + } + } + return results; +} + +std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig) { + std::vector<Clause> results; + for (size_t i = 0; i < c.literals_.size(); ++i) { + for (size_t j = i + 1; j < c.literals_.size(); ++j) { + if (c.literals_[i].is_positive_ != c.literals_[j].is_positive_) { + continue; // Must have same polarity + } + Substitution subst; + if (!unify(bank, c.literals_[i].atom_, c.literals_[j].atom_, subst, uconfig)) { + continue; + } + // Build factored clause: drop literal j, apply subst to all + Clause factored; + factored.rule_ = InferenceRule::kFactoring; + factored.parent1_ = c.id_; + for (size_t k = 0; k < c.literals_.size(); ++k) { + if (k != j) { + TermId const new_atom = applySubstitution(subst, c.literals_[k].atom_, bank); + factored.literals_.push_back( + {.atom_ = new_atom, .is_positive_ = c.literals_[k].is_positive_}); + } + } + results.push_back(std::move(factored)); + } + } + return results; +} + +} // namespace atp diff --git a/proofsearch/src/infer/substitution.cc b/proofsearch/src/infer/substitution.cc new file mode 100644 index 0000000..584008b --- /dev/null +++ b/proofsearch/src/infer/substitution.cc @@ -0,0 +1,119 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/infer/substitution.h" + +#include "atp/core/term.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +#include <algorithm> +#include <vector> + +namespace atp { + +bool Substitution::bind(TermId var, TermId term) { + auto [it, inserted] = bindings_.emplace(var, term); + if (!inserted) { + // Already bound — succeed only if bound to the same term + return it->second == term; + } + return true; +} + +TermId Substitution::lookup(TermId var) const { + auto it = bindings_.find(var); + if (it != bindings_.end()) { + return it->second; + } + return kInvalidId; +} + +TermId Substitution::resolve(TermId id, const TermBank& bank) const { + // Walk the chain: X → Y → Z → f(a) + // Stop when we hit a non-variable or an unbound variable. + while (bank.isVariable(id)) { + auto it = bindings_.find(id); + if (it == bindings_.end()) { + break; // Unbound variable — stop here + } + id = it->second; + } + return id; +} + +TermId Substitution::apply(TermId term, TermBank& bank) const { + // First, resolve through variable chain + term = resolve(term, bank); + + if (bank.isVariable(term)) { + // Free variable (unbound) — leave as-is + return term; + } + + // IMPORTANT: Copy symbol_id and args BEFORE recursing. + // Recursive apply() calls may trigger bank.makeTerm() → realloc → dangling ref. + const Term& t = bank.getTerm(term); + SymbolId const sym = t.symbol_id_; + std::vector<TermId> const old_args(t.args_); // copy! + + if (old_args.empty()) { + // Constant or 0-arity — no substitution needed + return term; + } + + // Recursively apply to all arguments + std::vector<TermId> new_args; + new_args.reserve(old_args.size()); + bool changed = false; + for (TermId const arg : old_args) { + TermId const new_arg = apply(arg, bank); + new_args.push_back(new_arg); + if (new_arg != arg) { + changed = true; + } + } + + if (!changed) { + return term; + } + + return bank.makeTerm(sym, new_args); +} + +bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const { + term = resolve(term, bank); + + if (var == term) { + return true; + } + + if (bank.isVariable(term)) { + return false; // Different unbound variable + } + + const Term& t = bank.getTerm(term); + return std::any_of(t.args_.begin(), t.args_.end(), + [&](TermId arg) { return occursIn(var, arg, bank); }); +} + +void Substitution::clear() { + bindings_.clear(); +} + +} // namespace atp
\ No newline at end of file diff --git a/proofsearch/src/infer/unification.cc b/proofsearch/src/infer/unification.cc new file mode 100644 index 0000000..c42bf67 --- /dev/null +++ b/proofsearch/src/infer/unification.cc @@ -0,0 +1,92 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/infer/unification.h" + +#include "atp/core/term.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/infer/substitution.h" + +#include <cstddef> +#include <vector> + +namespace atp { + +bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, + const UnificationConfig& config) { + t1 = subst.resolve(t1, bank); + t2 = subst.resolve(t2, bank); + + if (t1 == t2) { + return true; + } + + if (bank.isVariable(t1)) { + if (config.enable_occurs_check_ && subst.occursIn(t1, t2, bank)) { + return false; + } + subst.bind(t1, t2); + return true; + } + + if (bank.isVariable(t2)) { + if (config.enable_occurs_check_ && subst.occursIn(t2, t1, bank)) { + return false; + } + subst.bind(t2, t1); + return true; + } + + const Term& term1 = bank.getTerm(t1); + const Term& term2 = bank.getTerm(t2); + + if (term1.symbol_id_ != term2.symbol_id_ || term1.arity() != term2.arity()) { + return false; + } + + for (size_t i = 0; i < term1.arity(); ++i) { + if (!unify(bank, term1.args_[i], term2.args_[i], subst, config)) { + return false; + } + } + + return true; +} + +TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) { + term = subst.resolve(term, bank); + if (bank.isVariable(term)) { + return term; + } + + // IMPORTANT: Copy args and symbol_id BEFORE recursing. + // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs. + const Term& t = bank.getTerm(term); + SymbolId const sym = t.symbol_id_; + std::vector<TermId> const old_args(t.args_); // copy! + + std::vector<TermId> new_args; + new_args.reserve(old_args.size()); + for (TermId const arg : old_args) { + new_args.push_back(applySubstitution(subst, arg, bank)); + } + return bank.makeTerm(sym, new_args); +} + +} // namespace atp
\ No newline at end of file diff --git a/proofsearch/src/main.cc b/proofsearch/src/main.cc new file mode 100644 index 0000000..c683d39 --- /dev/null +++ b/proofsearch/src/main.cc @@ -0,0 +1,99 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +/// @file main.cc +/// @brief ATP Engine command-line entry point. + +#include "atp/core/clause_store.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/frontend/tptp_parser.h" +#include "atp/proof/proof_trace.h" +#include "atp/search/prover.h" + +#include <cstdlib> +#include <exception> +#include <iostream> +#include <string> +#include <utility> + +int main(int argc, char* argv[]) { + std::cerr << "richard-atp-engine Copyright (C) 2026 Richard Qin\n" + << "This program comes with ABSOLUTELY NO WARRANTY.\n" + << "This is free software, and you are welcome to redistribute it\n" + << "under certain conditions; see LICENSE for details.\n\n"; + + if (argc < 2) { + std::cerr << "Usage: atp <file.p>\n"; + return EXIT_FAILURE; + } + + const std::string filepath = argv[1]; + + try { + // 1. Initialize core modules + atp::SymbolTable symbols; + atp::TermBank bank(symbols); + atp::ClauseStore store; + + // 2. Parse TPTP input + auto problem = atp::parseTptpFile(filepath, bank, symbols); + + std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << filepath + << "\n"; + + // 3. Prepare clauses for proving + auto clauses = atp::prepareForProving(problem, bank, symbols); + + std::cerr << "% " << clauses.size() << " clauses prepared for proving\n"; + + // 4. Run the prover + atp::Prover prover(bank, store); + prover.addClauses(std::move(clauses)); + atp::ProverResult const result = prover.prove(); + + // 5. Output result (SZS format) + switch (result) { + case atp::ProverResult::kTheorem: { + std::cout << "% SZS status Theorem for " << filepath << "\n\n"; + + // Extract and print proof + auto eid = prover.getEmptyClauseId(); + if (eid.has_value()) { + auto proof = atp::extractProof(store, *eid); + std::cout << "% SZS output start Proof for " << filepath << "\n"; + std::cout << atp::formatProof(proof, store, bank); + std::cout << "% SZS output end Proof for " << filepath << "\n"; + } + break; + } + case atp::ProverResult::kSaturation: + std::cout << "% SZS status Satisfiable for " << filepath << "\n"; + break; + case atp::ProverResult::kTimeout: + std::cout << "% SZS status Timeout for " << filepath << "\n"; + break; + } + + } catch (const std::exception& e) { + std::cerr << "% Error: " << e.what() << "\n"; + return EXIT_FAILURE; + } + + return EXIT_SUCCESS; +} diff --git a/proofsearch/src/normalize/clausifier.cc b/proofsearch/src/normalize/clausifier.cc new file mode 100644 index 0000000..17c63f8 --- /dev/null +++ b/proofsearch/src/normalize/clausifier.cc @@ -0,0 +1,17 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ diff --git a/proofsearch/src/proof/proof_trace.cc b/proofsearch/src/proof/proof_trace.cc new file mode 100644 index 0000000..5fa4b04 --- /dev/null +++ b/proofsearch/src/proof/proof_trace.cc @@ -0,0 +1,249 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/proof/proof_trace.h" + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +#include <algorithm> +#include <cstddef> +#include <stack> +#include <string> +#include <unordered_map> +#include <unordered_set> +#include <vector> + +namespace atp { + +// extractProof +// DFS from empty clause back to axioms, collect all participating clauses, +// then reverse for topological order (axioms first). + +std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_clause_id) { + std::vector<ProofStep> steps; + std::unordered_set<ClauseId> visited; + std::stack<ClauseId> worklist; + worklist.push(empty_clause_id); + + while (!worklist.empty()) { + const ClauseId cid = worklist.top(); + worklist.pop(); + + if (cid == kInvalidId) { + continue; + } + if (visited.contains(cid)) { + continue; + } + visited.insert(cid); + + const Clause& c = store.getClause(cid); + steps.push_back({ + .clause_id_ = cid, + .rule_ = c.rule_, + .parent1_ = c.parent1_, + .parent2_ = c.parent2_, + }); + + // Recurse into parents (axioms have kInvalidId parents, which are + // filtered by the check at the top of the loop) + worklist.push(c.parent1_); + worklist.push(c.parent2_); + } + + // Reverse: axioms (leaves) first → empty clause (root) last + std::ranges::reverse(steps); + return steps; +} + +// termToString + +std::string termToString(TermId id, const TermBank& bank) { + const Term& t = bank.getTerm(id); + std::string name(bank.symbols().getName(t.symbol_id_)); + + if (t.args_.empty()) { + return name; + } + + std::string result = name + "("; + for (size_t i = 0; i < t.args_.size(); ++i) { + if (i > 0) { + result += ","; + } + result += termToString(t.args_[i], bank); + } + result += ")"; + return result; +} + +// Pretty variable names + +namespace { + +/// Generate a human-readable variable name from an index. +/// 0→X, 1→Y, 2→Z, 3→W, 4→V, 5→U, 6→X1, 7→Y1, ... +std::string prettyVarName(size_t index) { + constexpr size_t kBaseCount = 6; + const size_t base_index = index % kBaseCount; + const char base = [&]() { + switch (base_index) { + case 0: + return 'X'; + case 1: + return 'Y'; + case 2: + return 'Z'; + case 3: + return 'W'; + case 4: + return 'V'; + case 5: + return 'U'; + default: + return 'X'; + } + }(); + + const size_t suffix = index / kBaseCount; + if (suffix == 0) { + return std::string{base}; + } + return std::string{base} + std::to_string(suffix); +} + +/// Pretty-print a term, renaming variables to readable names. +/// `var_map` is built incrementally: each new variable gets the next name. +std::string termToPretty(TermId id, const TermBank& bank, + std::unordered_map<TermId, std::string>& var_map) { + if (bank.isVariable(id)) { + auto it = var_map.find(id); + if (it != var_map.end()) { + return it->second; + } + const std::string name = prettyVarName(var_map.size()); + var_map[id] = name; + return name; + } + + const Term& t = bank.getTerm(id); + std::string name(bank.symbols().getName(t.symbol_id_)); + + if (t.args_.empty()) { + return name; + } + + std::string result = name + "("; + for (size_t i = 0; i < t.args_.size(); ++i) { + if (i > 0) { + result += ","; + } + result += termToPretty(t.args_[i], bank, var_map); + } + result += ")"; + return result; +} + +// ruleToString + +std::string ruleToString(InferenceRule rule) { + switch (rule) { + case InferenceRule::kInput: + return "input"; + case InferenceRule::kResolution: + return "resolution"; + case InferenceRule::kFactoring: + return "factoring"; + default: + return "unknown"; + } +} + +} // namespace + +// clauseToString + +std::string clauseToString(const Clause& clause, const TermBank& bank) { + if (clause.isEmpty()) { + return "□"; + } + + // Per-clause variable renaming: _R109 → X, _R286 → Y, etc. + std::unordered_map<TermId, std::string> var_map; + + std::string result; + for (size_t i = 0; i < clause.literals_.size(); ++i) { + if (i > 0) { + result += " ∨ "; + } + if (!clause.literals_[i].is_positive_) { + result += "¬"; + } + result += termToPretty(clause.literals_[i].atom_, bank, var_map); + } + return result; +} + +// formatProof + +std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore& store, + const TermBank& bank) { + // Build a local renumbering: internal ClauseId → sequential proof step number + std::unordered_map<ClauseId, size_t> id_to_step; + for (size_t i = 0; i < proof.size(); ++i) { + id_to_step[proof[i].clause_id_] = i + 1; // 1-based + } + + auto local_name = [&](ClauseId cid) -> std::string { + auto it = id_to_step.find(cid); + if (it != id_to_step.end()) { + return std::to_string(it->second); + } + // Fallback: shouldn't happen in a valid proof + return "?" + std::to_string(cid); + }; + + std::string result; + for (size_t i = 0; i < proof.size(); ++i) { + const auto& step = proof[i]; + const Clause& c = store.getClause(step.clause_id_); + + result += std::to_string(i + 1) + ". "; + result += "[" + ruleToString(step.rule_) + "] "; + result += clauseToString(c, bank); + + // Show parents for derived clauses + if (step.parent1_ != kInvalidId) { + result += " [" + local_name(step.parent1_); + if (step.parent2_ != kInvalidId) { + result += ", " + local_name(step.parent2_); + } + result += "]"; + } + + result += "\n"; + } + return result; +} + +} // namespace atp diff --git a/proofsearch/src/rewrite/ordering.cc b/proofsearch/src/rewrite/ordering.cc new file mode 100644 index 0000000..17c63f8 --- /dev/null +++ b/proofsearch/src/rewrite/ordering.cc @@ -0,0 +1,17 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ diff --git a/proofsearch/src/rewrite/paramodulation.cc b/proofsearch/src/rewrite/paramodulation.cc new file mode 100644 index 0000000..17c63f8 --- /dev/null +++ b/proofsearch/src/rewrite/paramodulation.cc @@ -0,0 +1,17 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ diff --git a/proofsearch/src/search/prover.cc b/proofsearch/src/search/prover.cc new file mode 100644 index 0000000..f3f8bb0 --- /dev/null +++ b/proofsearch/src/search/prover.cc @@ -0,0 +1,167 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/search/prover.h" + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/infer/resolution.h" +#include "atp/infer/unification.h" +#include "atp/simplify/subsumption.h" +#include "atp/simplify/tautology.h" + +#include <algorithm> +#include <cstddef> +#include <cstdint> +#include <optional> +#include <utility> +#include <vector> + +namespace atp { + +Prover::Prover(TermBank& bank, ClauseStore& store, ProverConfig config) + : bank_(bank), store_(store), config_(std::move(config)), unprocessed_(config_.comparator_) {} + +void Prover::addClauses(std::vector<Clause> clauses) { + for (auto& clause : clauses) { + clause.depth_ = 0; + ClauseId const id = store_.addClause(clause); + unprocessed_.push(store_.getClause(id)); + } +} + +bool Prover::hitResourceLimit(size_t iterations) const { + return iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_; +} + +Clause Prover::popGivenClause() { + Clause given = unprocessed_.top(); + unprocessed_.pop(); + return given; +} + +bool Prover::isForwardSubsumedByProcessed(const Clause& clause) const { + return std::ranges::any_of(processed_, + [&](ClauseId pid) { return subsumes(store_.getClause(pid), clause); }); +} + +bool Prover::shouldSkipGiven(const Clause& given) const { + return isTautology(given) || isForwardSubsumedByProcessed(given); +} + +void Prover::applyBackwardSubsumption(const Clause& given) { + std::erase_if(processed_, [&](ClauseId pid) { return subsumes(given, store_.getClause(pid)); }); +} + +std::vector<Clause> Prover::generateNewClauses(const Clause& given) const { + std::vector<Clause> new_clauses; + const UnificationConfig uconfig{.enable_occurs_check_ = config_.enable_occurs_check_}; + + for (ClauseId const pid : processed_) { + const Clause& pc = store_.getClause(pid); + + auto resolvents1 = allResolvents(bank_, given, pc, uconfig); + auto resolvents2 = allResolvents(bank_, pc, given, uconfig); + + for (auto& r : resolvents1) { + new_clauses.push_back(std::move(r)); + } + for (auto& r : resolvents2) { + new_clauses.push_back(std::move(r)); + } + } + + auto factors = factor(bank_, given, uconfig); + for (auto& f : factors) { + new_clauses.push_back(std::move(f)); + } + + return new_clauses; +} + +uint16_t Prover::computeDepth(const Clause& clause) const { + uint32_t const d1 = (clause.parent1_ != kInvalidId) ? store_.getClause(clause.parent1_).depth_ : 0; + uint32_t const d2 = (clause.parent2_ != kInvalidId) ? store_.getClause(clause.parent2_).depth_ : 0; + return static_cast<uint16_t>(std::max(d1, d2) + 1); +} + +std::optional<ClauseId> Prover::processNewClauses(std::vector<Clause> new_clauses) { + for (auto& nc : new_clauses) { + if (nc.isEmpty()) { + return store_.addClause(std::move(nc)); + } + + if (isTautology(nc)) { + continue; + } + + nc.depth_ = computeDepth(nc); + + ClauseId const nid = store_.addClause(nc); + const Clause& stored_nc = store_.getClause(nid); + if (isForwardSubsumedByProcessed(stored_nc)) { + continue; + } + + unprocessed_.push(stored_nc); + } + + return std::nullopt; +} + +ProverResult Prover::prove() { + size_t iterations = 0; + + while (!unprocessed_.empty()) { + if (hitResourceLimit(iterations)) { + return ProverResult::kTimeout; + } + ++iterations; + + Clause given = popGivenClause(); + + if (given.isEmpty()) { + empty_clause_id_ = given.id_; + return ProverResult::kTheorem; + } + + if (shouldSkipGiven(given)) { + continue; + } + + applyBackwardSubsumption(given); + std::vector<Clause> new_clauses = generateNewClauses(given); + processed_.push_back(given.id_); + + const std::optional<ClauseId> derived_empty = processNewClauses(std::move(new_clauses)); + if (derived_empty.has_value()) { + empty_clause_id_ = derived_empty; + return ProverResult::kTheorem; + } + } + + return ProverResult::kSaturation; +} + +std::optional<ClauseId> Prover::getEmptyClauseId() const { + return empty_clause_id_; +} + +} // namespace atp
\ No newline at end of file diff --git a/proofsearch/src/simplify/subsumption.cc b/proofsearch/src/simplify/subsumption.cc new file mode 100644 index 0000000..0038ad1 --- /dev/null +++ b/proofsearch/src/simplify/subsumption.cc @@ -0,0 +1,43 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/simplify/subsumption.h" + +#include "atp/core/clause.h" + +namespace atp { + +bool subsumes(const Clause& general, const Clause& specific) { + if (general.size() > specific.size()) { + return false; + } + for (const auto& lit_g : general.literals_) { + bool found = false; + for (const auto& lit_s : specific.literals_) { + if (lit_g.atom_ == lit_s.atom_ && lit_g.is_positive_ == lit_s.is_positive_) { + found = true; + break; + } + } + if (!found) { + return false; + } + } + return true; +} +} // namespace atp diff --git a/proofsearch/src/simplify/tautology.cc b/proofsearch/src/simplify/tautology.cc new file mode 100644 index 0000000..e35d874 --- /dev/null +++ b/proofsearch/src/simplify/tautology.cc @@ -0,0 +1,37 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/simplify/tautology.h" + +#include "atp/core/clause.h" + +#include <cstddef> + +namespace atp { +bool isTautology(const Clause& clause) { + for (size_t i = 0; i < clause.size(); ++i) { + for (size_t j = i + 1; j < clause.size(); ++j) { + if (clause.literals_[i].atom_ == clause.literals_[j].atom_ && + clause.literals_[i].is_positive_ != clause.literals_[j].is_positive_) { + return true; + } + } + } + return false; +} +} // namespace atp
\ No newline at end of file diff --git a/proofsearch/src/strategy/problem_analyzer.cc b/proofsearch/src/strategy/problem_analyzer.cc new file mode 100644 index 0000000..17c63f8 --- /dev/null +++ b/proofsearch/src/strategy/problem_analyzer.cc @@ -0,0 +1,17 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ diff --git a/proofsearch/tests/CMakeLists.txt b/proofsearch/tests/CMakeLists.txt new file mode 100644 index 0000000..184357b --- /dev/null +++ b/proofsearch/tests/CMakeLists.txt @@ -0,0 +1,31 @@ +# ─── GoogleTest ─────────────────────────────────────────────────────────────── +include(FetchContent) +FetchContent_Declare( + googletest + GIT_REPOSITORY https://github.com/google/googletest.git + GIT_TAG v1.14.0 +) +# Prevent GoogleTest from overriding our compiler/linker options +set(gtest_force_shared_crt ON CACHE BOOL "" FORCE) +FetchContent_MakeAvailable(googletest) + +include(GoogleTest) + +# ─── Helper: define a test target ──────────────────────────────────────────── +function(atp_add_test TEST_NAME TEST_SOURCE) + add_executable(${TEST_NAME} ${TEST_SOURCE}) + target_link_libraries(${TEST_NAME} PRIVATE atp_core GTest::gtest_main) + target_compile_options(${TEST_NAME} PRIVATE ${ATP_PROJECT_WARNING_FLAGS}) + gtest_discover_tests(${TEST_NAME}) +endfunction() + +# ─── Test Targets ──────────────────────────────────────────────────────────── +atp_add_test(test_term_bank test_term_bank.cc) +atp_add_test(test_unification test_unification.cc) +atp_add_test(test_clausifier test_clausifier.cc) +atp_add_test(test_resolution test_resolution.cc) +atp_add_test(test_discrim_tree test_discrim_tree.cc) +atp_add_test(test_prover test_prover.cc) +atp_add_test(test_simplify test_simplify.cc) +atp_add_test(test_proof_trace test_proof_trace.cc) +atp_add_test(test_end_to_end test_end_to_end.cc) diff --git a/proofsearch/tests/test_clausifier.cc b/proofsearch/tests/test_clausifier.cc new file mode 100644 index 0000000..17c63f8 --- /dev/null +++ b/proofsearch/tests/test_clausifier.cc @@ -0,0 +1,17 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ diff --git a/proofsearch/tests/test_discrim_tree.cc b/proofsearch/tests/test_discrim_tree.cc new file mode 100644 index 0000000..17c63f8 --- /dev/null +++ b/proofsearch/tests/test_discrim_tree.cc @@ -0,0 +1,17 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ diff --git a/proofsearch/tests/test_end_to_end.cc b/proofsearch/tests/test_end_to_end.cc new file mode 100644 index 0000000..ceb9991 --- /dev/null +++ b/proofsearch/tests/test_end_to_end.cc @@ -0,0 +1,184 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +/// @file test_end_to_end.cc +/// @brief End-to-end tests: TPTP string → parse → prove → verify result. + +#include "atp/core/clause_store.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/frontend/tptp_parser.h" +#include "atp/proof/proof_trace.h" +#include "atp/search/prover.h" + +#include <gtest/gtest.h> +#include <string> +#include <utility> + +namespace atp { +namespace { + +/// Helper: parse a TPTP string and run the prover, return the result. +struct E2EResult { + ProverResult result_; + std::string proof_output_; +}; + +E2EResult runProver(const std::string& tptp_input) { + SymbolTable symbols; + TermBank bank(symbols); + ClauseStore store; + + auto problem = parseTptpString(tptp_input, bank, symbols); + auto clauses = prepareForProving(problem, bank, symbols); + + Prover prover(bank, store); + prover.addClauses(std::move(clauses)); + ProverResult const result = prover.prove(); + + std::string proof_output; + if (result == ProverResult::kTheorem) { + auto eid = prover.getEmptyClauseId(); + if (eid.has_value()) { + auto proof = extractProof(store, *eid); + proof_output = formatProof(proof, store, bank); + } + } + + return {result, proof_output}; +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Simple Propositional +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(EndToEnd, SimplePropositional) { + auto [result, proof] = runProver(R"( + cnf(fact, axiom, p(a)). + cnf(rule, axiom, ~p(X) | q(X)). + cnf(goal, negated_conjecture, ~q(a)). + )"); + + EXPECT_EQ(result, ProverResult::kTheorem); + EXPECT_FALSE(proof.empty()); + // Proof should contain the key elements + EXPECT_NE(proof.find("p(a)"), std::string::npos) << proof; + EXPECT_NE(proof.find("q(a)"), std::string::npos) << proof; +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Trivial: direct contradiction +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(EndToEnd, DirectContradiction) { + auto [result, proof] = runProver(R"( + cnf(pos, axiom, p(a)). + cnf(neg, negated_conjecture, ~p(a)). + )"); + + EXPECT_EQ(result, ProverResult::kTheorem); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Satisfiable: no contradiction possible +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(EndToEnd, Satisfiable) { + auto [result, proof] = runProver(R"( + cnf(a1, axiom, p(a)). + cnf(a2, axiom, q(b)). + )"); + + EXPECT_EQ(result, ProverResult::kSaturation); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Three-step chain +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(EndToEnd, ThreeStepChain) { + auto [result, proof] = runProver(R"( + cnf(a1, axiom, p(a)). + cnf(a2, axiom, ~p(X) | q(X)). + cnf(a3, axiom, ~q(X) | r(X)). + cnf(goal, negated_conjecture, ~r(a)). + )"); + + EXPECT_EQ(result, ProverResult::kTheorem); + EXPECT_NE(proof.find("r(a)"), std::string::npos) << proof; +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Proof output format +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(EndToEnd, ProofOutputContainsAllSteps) { + auto [result, proof] = runProver(R"( + cnf(fact, axiom, p(a)). + cnf(rule, axiom, ~p(X) | q(X)). + cnf(goal, negated_conjecture, ~q(a)). + )"); + + ASSERT_EQ(result, ProverResult::kTheorem); + + // Must contain [input] lines for axioms + EXPECT_NE(proof.find("[input]"), std::string::npos) << proof; + // Must contain [resolution] for derived clauses + EXPECT_NE(proof.find("[resolution]"), std::string::npos) << proof; + // Must contain empty clause marker + std::string const empty_marker = "□"; + EXPECT_NE(proof.find(empty_marker), std::string::npos) << proof; + // Must contain [X, Y] provenance (sequential numbers) + EXPECT_NE(proof.find('['), std::string::npos) << proof; +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Monkey and Banana Problem (the flagship test!) +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(EndToEnd, MonkeyBanana) { + auto [result, proof] = runProver(R"( + % Initial state + cnf(init_state, axiom, state(a, b, c, h0, s0)). + + % Action: Go(X) + cnf(action_go, axiom, ~state(M, B, G, h0, S) | state(X, B, G, h0, do(go(X), S))). + + % Action: Push(X) + cnf(action_push, axiom, ~state(M, M, G, h0, S) | state(X, X, G, h0, do(push(X), S))). + + % Action: Climb + cnf(action_climb, axiom, ~state(M, M, G, h0, S) | state(M, M, G, h1, do(climb, S))). + + % Action: Down + cnf(action_down, axiom, ~state(M, B, G, h1, S) | state(M, B, G, h0, do(down, S))). + + % Action: Reach + cnf(action_reach, axiom, ~state(G, G, G, h1, S) | goal_reached(do(reach, S))). + + % Negated goal + cnf(negated_goal, negated_conjecture, ~goal_reached(S)). + )"); + + EXPECT_EQ(result, ProverResult::kTheorem) << "ATP should prove the monkey can get the banana!\n" + << "Proof output:\n" + << proof; +} + +} // namespace +} // namespace atp diff --git a/proofsearch/tests/test_proof_trace.cc b/proofsearch/tests/test_proof_trace.cc new file mode 100644 index 0000000..f2c3c96 --- /dev/null +++ b/proofsearch/tests/test_proof_trace.cc @@ -0,0 +1,207 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/literal.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/proof/proof_trace.h" +#include "atp/search/prover.h" + +#include <gtest/gtest.h> +#include <string> +#include <utility> +#include <vector> + +namespace atp { +namespace { + +class ProofTraceTest : public ::testing::Test { + protected: + SymbolTable symbols_; + TermBank bank_{symbols_}; + ClauseStore store_; + + SymbolId sym_a_{}, sym_b_{}; + SymbolId sym_p_{}, sym_q_{}; + SymbolId sym_x_{}; + + TermId a_term_{}, b_term_{}, x_term_{}; + + void SetUp() override { + sym_a_ = symbols_.intern("a", SymbolKind::kConstant); + sym_b_ = symbols_.intern("b", SymbolKind::kConstant); + sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1); + sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1); + sym_x_ = symbols_.intern("X", SymbolKind::kVariable); + + a_term_ = bank_.makeTerm(sym_a_, {}); + b_term_ = bank_.makeTerm(sym_b_, {}); + x_term_ = bank_.makeVar(sym_x_); + } + + TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); } + TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); } + + static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; } + static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; } + + static Clause makeClause(std::vector<Literal> lits) { + Clause cl; + cl.literals_ = std::move(lits); + return cl; + } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// termToString Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProofTraceTest, TermToStringConstant) { + EXPECT_EQ(termToString(a_term_, bank_), "a"); +} + +TEST_F(ProofTraceTest, TermToStringVariable) { + EXPECT_EQ(termToString(x_term_, bank_), "X"); +} + +TEST_F(ProofTraceTest, TermToStringCompound) { + TermId const pa = p(a_term_); + EXPECT_EQ(termToString(pa, bank_), "P(a)"); +} + +TEST_F(ProofTraceTest, TermToStringNested) { + SymbolId const sym_f = symbols_.intern("f", SymbolKind::kFunction, 1); + TermId const fa = bank_.makeTerm(sym_f, {{a_term_}}); + TermId const pfa = p(fa); + EXPECT_EQ(termToString(pfa, bank_), "P(f(a))"); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// clauseToString Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProofTraceTest, ClauseToStringEmpty) { + Clause const empty = makeClause({}); + EXPECT_EQ(clauseToString(empty, bank_), "□"); +} + +TEST_F(ProofTraceTest, ClauseToStringSinglePositive) { + Clause const c = makeClause({pos(p(a_term_))}); + EXPECT_EQ(clauseToString(c, bank_), "P(a)"); +} + +TEST_F(ProofTraceTest, ClauseToStringSingleNegative) { + Clause const c = makeClause({neg(p(a_term_))}); + EXPECT_EQ(clauseToString(c, bank_), "¬P(a)"); +} + +TEST_F(ProofTraceTest, ClauseToStringMultipleLiterals) { + Clause const c = makeClause({neg(p(x_term_)), pos(q(x_term_))}); + std::string const s = clauseToString(c, bank_); + EXPECT_EQ(s, "¬P(X) ∨ Q(X)"); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// extractProof Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProofTraceTest, ExtractProofTrivial) { + // Run a trivial proof: {P(a)} + {¬P(a)} → □ + Prover prover(bank_, store_); + prover.addClauses({makeClause({pos(p(a_term_))}), makeClause({neg(p(a_term_))})}); + ProverResult const result = prover.prove(); + ASSERT_EQ(result, ProverResult::kTheorem); + + auto eid = prover.getEmptyClauseId(); + ASSERT_TRUE(eid.has_value()); + + auto proof = extractProof(store_, *eid); + ASSERT_GE(proof.size(), 3U); // At least: 2 axioms + 1 empty clause + + // First steps should be axioms (kInput) + EXPECT_EQ(proof.front().rule_, InferenceRule::kInput); + // Last step should be the empty clause + EXPECT_EQ(proof.back().clause_id_, *eid); + // Last step should be resolution + EXPECT_EQ(proof.back().rule_, InferenceRule::kResolution); +} + +TEST_F(ProofTraceTest, ExtractProofTwoStep) { + // {P(a)}, {¬P(X), Q(X)}, {¬Q(a)} → □ in 2 resolution steps + Prover prover(bank_, store_); + prover.addClauses({makeClause({pos(p(a_term_))}), makeClause({neg(p(x_term_)), pos(q(x_term_))}), + makeClause({neg(q(a_term_))})}); + ProverResult const result = prover.prove(); + ASSERT_EQ(result, ProverResult::kTheorem); + + auto eid = prover.getEmptyClauseId(); + ASSERT_TRUE(eid.has_value()); + + auto proof = extractProof(store_, *eid); + // Should have axioms + intermediate + empty clause + ASSERT_GE(proof.size(), 4U); // 3 axioms + at least 1 intermediate + empty + + // Last step is the empty clause + EXPECT_EQ(proof.back().clause_id_, *eid); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// formatProof Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProofTraceTest, FormatProofContainsExpectedElements) { + Prover prover(bank_, store_); + prover.addClauses({makeClause({pos(p(a_term_))}), makeClause({neg(p(a_term_))})}); + prover.prove(); + + auto eid = prover.getEmptyClauseId(); + ASSERT_TRUE(eid.has_value()); + + auto proof = extractProof(store_, *eid); + std::string const output = formatProof(proof, store_, bank_); + + // Should contain key elements + EXPECT_NE(output.find("input"), std::string::npos) << output; + EXPECT_NE(output.find("resolution"), std::string::npos) << output; + EXPECT_NE(output.find("P(a)"), std::string::npos) << output; + // Empty clause should appear + std::string const empty_marker = "□"; + EXPECT_NE(output.find(empty_marker), std::string::npos) << output; +} + +TEST_F(ProofTraceTest, FormatProofNoParentsForAxioms) { + Prover prover(bank_, store_); + prover.addClauses({makeClause({pos(p(a_term_))}), makeClause({neg(p(a_term_))})}); + prover.prove(); + + auto eid = prover.getEmptyClauseId(); + auto proof = extractProof(store_, *eid); + std::string const output = formatProof(proof, store_, bank_); + + // The first line (an axiom) should NOT have "[from ...]" + // Find the first newline + auto first_line = output.substr(0, output.find('\n')); + EXPECT_EQ(first_line.find("[from"), std::string::npos) + << "Axiom should not have parent info: " << first_line; +} + +} // namespace +} // namespace atp diff --git a/proofsearch/tests/test_prover.cc b/proofsearch/tests/test_prover.cc new file mode 100644 index 0000000..74d02ad --- /dev/null +++ b/proofsearch/tests/test_prover.cc @@ -0,0 +1,183 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/literal.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/search/prover.h" + +#include <gtest/gtest.h> +#include <utility> +#include <vector> + +namespace atp { +namespace { + +class ProverTest : public ::testing::Test { + protected: + SymbolTable symbols_; + TermBank bank_{symbols_}; + ClauseStore store_; + + SymbolId sym_a_{}, sym_b_{}; + SymbolId sym_f_{}; + SymbolId sym_p_{}, sym_q_{}, sym_r_{}; + SymbolId sym_x_{}, sym_y_{}; + + TermId a_{}, b_{}, x_{}, y_{}; + + + void SetUp() override { + sym_a_ = symbols_.intern("a", SymbolKind::kConstant); + sym_b_ = symbols_.intern("b", SymbolKind::kConstant); + sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1); + sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1); + sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1); + sym_r_ = symbols_.intern("R", SymbolKind::kPredicate, 2); + sym_x_ = symbols_.intern("X", SymbolKind::kVariable); + sym_y_ = symbols_.intern("Y", SymbolKind::kVariable); + + a_ = bank_.makeTerm(sym_a_, {}); + b_ = bank_.makeTerm(sym_b_, {}); + x_ = bank_.makeVar(sym_x_); + y_ = bank_.makeVar(sym_y_); + } + + TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); } + TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); } + TermId r(TermId a1, TermId a2) { return bank_.makeTerm(sym_r_, {{a1, a2}}); } + TermId f(TermId arg) { return bank_.makeTerm(sym_f_, {{arg}}); } + + static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; } + static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; } + + static Clause makeClause(std::vector<Literal> lits) { + Clause cl; + cl.literals_ = std::move(lits); + return cl; + } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// Trivial refutation: {P(a)} and {¬P(a)} → empty clause +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProverTest, TrivialRefutation) { + Prover prover(bank_, store_); + prover.addClauses({makeClause({pos(p(a_))}), makeClause({neg(p(a_))})}); + + const ProverResult kResult = prover.prove(); + EXPECT_EQ(kResult, ProverResult::kTheorem); + EXPECT_TRUE(prover.getEmptyClauseId().has_value()); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Unification required: {P(X)} and {¬P(a)} → empty clause +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProverTest, RefutationWithUnification) { + Prover prover(bank_, store_); + prover.addClauses({makeClause({pos(p(x_))}), makeClause({neg(p(a_))})}); + + const ProverResult kResult = prover.prove(); + EXPECT_EQ(kResult, ProverResult::kTheorem); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Multi-step: {P(a)}, {¬P(X), Q(X)}, {¬Q(a)} +// Step 1: resolve P(a) with ¬P(X)∨Q(X) → Q(a) +// Step 2: resolve Q(a) with ¬Q(a) → empty +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProverTest, TwoStepRefutation) { + Prover prover(bank_, store_); + prover.addClauses( + {makeClause({pos(p(a_))}), makeClause({neg(p(x_)), pos(q(x_))}), makeClause({neg(q(a_))})}); + + const ProverResult kResult = prover.prove(); + EXPECT_EQ(kResult, ProverResult::kTheorem); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Saturation: {P(a)}, {Q(b)} — no complementary literals +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProverTest, Saturation) { + Prover prover(bank_, store_); + prover.addClauses({makeClause({pos(p(a_))}), makeClause({pos(q(b_))})}); + + const ProverResult kResult = prover.prove(); + EXPECT_EQ(kResult, ProverResult::kSaturation); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Timeout: set very low limits +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProverTest, Timeout) { + ProverConfig config; + config.max_iterations_ = 1; + + // Need enough clauses to not saturate in 1 iteration + Prover prover(bank_, store_, config); + prover.addClauses({makeClause({pos(p(x_)), pos(q(x_))}), makeClause({neg(p(a_)), pos(q(a_))}), + makeClause({neg(q(x_)), pos(p(f(x_)))}), makeClause({neg(p(x_)), neg(q(x_))})}); + + const ProverResult kResult = prover.prove(); + EXPECT_EQ(kResult, ProverResult::kTimeout); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Chain reasoning: P(a), ¬P(X)∨Q(X), ¬Q(X)∨R(X), ¬R(a) +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProverTest, ThreeStepChain) { + const SymbolId kSymS = symbols_.intern("S", SymbolKind::kPredicate, 1); + auto s = [&](TermId arg) { return bank_.makeTerm(kSymS, {{arg}}); }; + + Prover prover(bank_, store_); + prover.addClauses({ + makeClause({pos(p(a_))}), // P(a) + makeClause({neg(p(x_)), pos(q(x_))}), // ¬P(X) ∨ Q(X) + makeClause({neg(q(x_)), pos(s(x_))}), // ¬Q(X) ∨ S(X) + makeClause({neg(s(a_))}) // ¬S(a) + }); + + const ProverResult kResult = prover.prove(); + EXPECT_EQ(kResult, ProverResult::kTheorem); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Empty clause in input directly +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ProverTest, EmptyClauseInInput) { + Prover prover(bank_, store_); + prover.addClauses({makeClause({}), // empty clause directly + makeClause({pos(p(a_))})}); + + // Empty clause should be detected immediately when selected from queue + const ProverResult kResult = prover.prove(); + EXPECT_EQ(kResult, ProverResult::kTheorem); +} + +} // namespace +} // namespace atp diff --git a/proofsearch/tests/test_resolution.cc b/proofsearch/tests/test_resolution.cc new file mode 100644 index 0000000..02250d9 --- /dev/null +++ b/proofsearch/tests/test_resolution.cc @@ -0,0 +1,257 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/clause.h" +#include "atp/core/literal.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/infer/resolution.h" + +#include <gtest/gtest.h> +#include <utility> +#include <vector> + +namespace atp { +namespace { + +class ResolutionTest : public ::testing::Test { + protected: + SymbolTable symbols_; + TermBank bank_{symbols_}; + + SymbolId sym_a_{}, sym_b_{}, sym_c_{}; + SymbolId sym_f_{}; + SymbolId sym_p_{}, sym_q_{}, sym_r_{}; + SymbolId sym_x_{}, sym_y_{}, sym_z_{}; + + TermId a_{}, b_{}, c_{}; + TermId x_{}, y_{}, z_{}; + + void SetUp() override { + sym_a_ = symbols_.intern("a", SymbolKind::kConstant); + sym_b_ = symbols_.intern("b", SymbolKind::kConstant); + sym_c_ = symbols_.intern("c", SymbolKind::kConstant); + sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1); + sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1); + sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1); + sym_r_ = symbols_.intern("R", SymbolKind::kPredicate, 2); + sym_x_ = symbols_.intern("X", SymbolKind::kVariable); + sym_y_ = symbols_.intern("Y", SymbolKind::kVariable); + sym_z_ = symbols_.intern("Z", SymbolKind::kVariable); + + a_ = bank_.makeTerm(sym_a_, {}); + b_ = bank_.makeTerm(sym_b_, {}); + c_ = bank_.makeTerm(sym_c_, {}); + x_ = bank_.makeVar(sym_x_); + y_ = bank_.makeVar(sym_y_); + z_ = bank_.makeVar(sym_z_); + } + + TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); } + TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); } + TermId r(TermId a1, TermId a2) { return bank_.makeTerm(sym_r_, {{a1, a2}}); } + TermId f(TermId arg) { return bank_.makeTerm(sym_f_, {{arg}}); } + + // Helper: make a clause from literals + static Clause makeClause(std::vector<Literal> lits, ClauseId id = kInvalidId) { + Clause c; + c.id_ = id; + c.literals_ = std::move(lits); + return c; + } + + static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; } + static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// Basic Resolution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ResolutionTest, SimpleGroundResolution) { + // {P(a)} and {¬P(a), Q(b)} → {Q(b)} + Clause const c1 = makeClause({pos(p(a_))}, 0); + Clause const c2 = makeClause({neg(p(a_)), pos(q(b_))}, 1); + + auto result = resolve(bank_, c1, 0, c2, 0); + ASSERT_TRUE(result.has_value()); + EXPECT_EQ(result->literals_.size(), 1); + EXPECT_EQ(result->literals_[0].atom_, q(b_)); + EXPECT_TRUE(result->literals_[0].is_positive_); +} + +TEST_F(ResolutionTest, ResolutionWithUnification) { + // {P(X)} and {¬P(a)} → {} (empty clause!) + Clause const c1 = makeClause({pos(p(x_))}, 0); + Clause const c2 = makeClause({neg(p(a_))}, 1); + + auto result = resolve(bank_, c1, 0, c2, 0); + ASSERT_TRUE(result.has_value()); + EXPECT_TRUE(result->isEmpty()) << "Should derive empty clause (contradiction)"; +} + +TEST_F(ResolutionTest, ResolutionFailsSamePolarity) { + // {P(a)} and {P(b)} → no resolution (both positive) + Clause const c1 = makeClause({pos(p(a_))}, 0); + Clause const c2 = makeClause({pos(p(b_))}, 1); + + auto result = resolve(bank_, c1, 0, c2, 0); + EXPECT_FALSE(result.has_value()); +} + +TEST_F(ResolutionTest, ResolutionFailsNoUnifier) { + // {P(a)} and {¬P(b)} → can't unify a with b + Clause const c1 = makeClause({pos(p(a_))}, 0); + Clause const c2 = makeClause({neg(p(b_))}, 1); + + auto result = resolve(bank_, c1, 0, c2, 0); + EXPECT_FALSE(result.has_value()); +} + +TEST_F(ResolutionTest, ResolutionAppliesSubstToRemainingLiterals) { + // {P(X), Q(X)} and {¬P(a)} → {Q(a)} + Clause const c1 = makeClause({pos(p(x_)), pos(q(x_))}, 0); + Clause const c2 = makeClause({neg(p(a_))}, 1); + + auto result = resolve(bank_, c1, 0, c2, 0); + ASSERT_TRUE(result.has_value()); + EXPECT_EQ(result->literals_.size(), 1); + EXPECT_EQ(result->literals_[0].atom_, q(a_)); +} + +TEST_F(ResolutionTest, ResolutionMultipleLiterals) { + // {P(X), Q(b)} and {¬P(a), R(a, c)} → {Q(b), R(a, c)} + Clause const c1 = makeClause({pos(p(x_)), pos(q(b_))}, 0); + Clause const c2 = makeClause({neg(p(a_)), pos(r(a_, c_))}, 1); + + auto result = resolve(bank_, c1, 0, c2, 0); + ASSERT_TRUE(result.has_value()); + EXPECT_EQ(result->literals_.size(), 2); +} + +TEST_F(ResolutionTest, VariableRenamingWorks) { + // Both clauses use variable X + // {P(X)} and {¬P(X), Q(X)} → {Q(a)} only if X is renamed in c2 + Clause const c1 = makeClause({pos(p(a_))}, 0); + Clause const c2 = makeClause({neg(p(x_)), pos(q(x_))}, 1); + + auto result = resolve(bank_, c1, 0, c2, 0); + ASSERT_TRUE(result.has_value()); + EXPECT_EQ(result->literals_.size(), 1); + // Q(X) should become Q(a) after substitution {X→a} + EXPECT_EQ(result->literals_[0].atom_, q(a_)); +} + +TEST_F(ResolutionTest, VariableRenamingPreventsClash) { + // {R(X, a)} and {¬R(b, X)} + // Without renaming: X would clash between c1 and c2 + // With renaming: c2's X → _R0, then unify R(X,a) with R(b,_R0) → {X→b, _R0→a} + Clause const c1 = makeClause({pos(r(x_, a_))}, 0); + Clause const c2 = makeClause({neg(r(b_, x_))}, 1); + + auto result = resolve(bank_, c1, 0, c2, 0); + ASSERT_TRUE(result.has_value()); + EXPECT_TRUE(result->isEmpty()); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// AllResolvents Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ResolutionTest, AllResolventsFindsAll) { + // {P(a), Q(a)} and {¬P(a), ¬Q(a)} + // Can resolve on P or Q → 2 resolvents + Clause const c1 = makeClause({pos(p(a_)), pos(q(a_))}, 0); + Clause const c2 = makeClause({neg(p(a_)), neg(q(a_))}, 1); + + auto results = allResolvents(bank_, c1, c2); + EXPECT_EQ(results.size(), 2); +} + +TEST_F(ResolutionTest, AllResolventsEmpty) { + // {P(a)} and {Q(b)} → no complementary pairs + Clause const c1 = makeClause({pos(p(a_))}, 0); + Clause const c2 = makeClause({pos(q(b_))}, 1); + + auto results = allResolvents(bank_, c1, c2); + EXPECT_TRUE(results.empty()); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Factoring Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ResolutionTest, SimpleFactoring) { + // {P(X), P(a), Q(X)} → factor P(X) with P(a): {P(a), Q(a)} + Clause const c = makeClause({pos(p(x_)), pos(p(a_)), pos(q(x_))}, 0); + + auto results = factor(bank_, c); + ASSERT_EQ(results.size(), 1); + EXPECT_EQ(results[0].literals_.size(), 2); + // After factoring: {P(a), Q(a)} + EXPECT_EQ(results[0].literals_[0].atom_, p(a_)); + EXPECT_EQ(results[0].literals_[1].atom_, q(a_)); +} + +TEST_F(ResolutionTest, NoFactoring) { + // {P(a), Q(b)} → different predicates, can't factor + Clause const c = makeClause({pos(p(a_)), pos(q(b_))}, 0); + auto results = factor(bank_, c); + EXPECT_TRUE(results.empty()); +} + +TEST_F(ResolutionTest, FactoringDifferentPolarity) { + // {P(a), ¬P(a)} → different polarity, can't factor + Clause const c = makeClause({pos(p(a_)), neg(p(a_))}, 0); + auto results = factor(bank_, c); + EXPECT_TRUE(results.empty()); +} + +TEST_F(ResolutionTest, FactoringNonUnifiable) { + // {P(a), P(b)} → can't unify a with b + Clause const c = makeClause({pos(p(a_)), pos(p(b_))}, 0); + auto results = factor(bank_, c); + EXPECT_TRUE(results.empty()); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Provenance Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(ResolutionTest, ResolventHasProvenance) { + Clause const c1 = makeClause({pos(p(x_))}, 5); + Clause const c2 = makeClause({neg(p(a_))}, 7); + + auto result = resolve(bank_, c1, 0, c2, 0); + ASSERT_TRUE(result.has_value()); + EXPECT_EQ(result->rule_, InferenceRule::kResolution); + EXPECT_EQ(result->parent1_, 5); + EXPECT_EQ(result->parent2_, 7); +} + +TEST_F(ResolutionTest, FactoredHasProvenance) { + Clause const c = makeClause({pos(p(x_)), pos(p(a_))}, 3); + auto results = factor(bank_, c); + ASSERT_FALSE(results.empty()); + EXPECT_EQ(results[0].rule_, InferenceRule::kFactoring); + EXPECT_EQ(results[0].parent1_, 3); +} + +} // namespace +} // namespace atp diff --git a/proofsearch/tests/test_simplify.cc b/proofsearch/tests/test_simplify.cc new file mode 100644 index 0000000..968ab3b --- /dev/null +++ b/proofsearch/tests/test_simplify.cc @@ -0,0 +1,191 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/clause.h" +#include "atp/core/literal.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/simplify/subsumption.h" +#include "atp/simplify/tautology.h" + +#include <gtest/gtest.h> +#include <utility> +#include <vector> + +namespace atp { +namespace { + +class SimplifyTest : public ::testing::Test { + protected: + SymbolTable symbols_; + TermBank bank_{symbols_}; + + SymbolId sym_a_{}, sym_b_{}, sym_c_{}; + SymbolId sym_p_{}, sym_q_{}, sym_r_{}; + SymbolId sym_x_{}; + + TermId a_{}, b_{}, c_{}, x_{}; + + void SetUp() override { + sym_a_ = symbols_.intern("a", SymbolKind::kConstant); + sym_b_ = symbols_.intern("b", SymbolKind::kConstant); + sym_c_ = symbols_.intern("c", SymbolKind::kConstant); + sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 1); + sym_q_ = symbols_.intern("Q", SymbolKind::kPredicate, 1); + sym_r_ = symbols_.intern("R", SymbolKind::kPredicate, 2); + sym_x_ = symbols_.intern("X", SymbolKind::kVariable); + + a_ = bank_.makeTerm(sym_a_, {}); + b_ = bank_.makeTerm(sym_b_, {}); + c_ = bank_.makeTerm(sym_c_, {}); + x_ = bank_.makeVar(sym_x_); + } + + TermId p(TermId arg) { return bank_.makeTerm(sym_p_, {{arg}}); } + TermId q(TermId arg) { return bank_.makeTerm(sym_q_, {{arg}}); } + TermId r(TermId a1, TermId a2) { return bank_.makeTerm(sym_r_, {{a1, a2}}); } + + static Literal pos(TermId atom) { return {.atom_ = atom, .is_positive_ = true}; } + static Literal neg(TermId atom) { return {.atom_ = atom, .is_positive_ = false}; } + + static Clause makeClause(std::vector<Literal> lits) { + Clause cl; + cl.literals_ = std::move(lits); + return cl; + } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// Tautology Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(SimplifyTest, TautologyComplementaryLiterals) { + // {P(a), ¬P(a)} → tautology + Clause const cl = makeClause({pos(p(a_)), neg(p(a_))}); + EXPECT_TRUE(isTautology(cl)); +} + +TEST_F(SimplifyTest, TautologyWithExtraLiterals) { + // {Q(b), P(a), ¬P(a)} → tautology + Clause const cl = makeClause({pos(q(b_)), pos(p(a_)), neg(p(a_))}); + EXPECT_TRUE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologySamePolarity) { + // {P(a), P(a)} → NOT tautology (same polarity) + Clause const cl = makeClause({pos(p(a_)), pos(p(a_))}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologyDifferentAtoms) { + // {P(a), ¬P(b)} → NOT tautology (different atoms) + Clause const cl = makeClause({pos(p(a_)), neg(p(b_))}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologyDifferentPredicates) { + // {P(a), ¬Q(a)} → NOT tautology (different predicates) + Clause const cl = makeClause({pos(p(a_)), neg(q(a_))}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologyEmptyClause) { + Clause const cl = makeClause({}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologySingleLiteral) { + Clause const cl = makeClause({pos(p(a_))}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, TautologyVariableAtom) { + // {P(X), ¬P(X)} → tautology (same variable term) + Clause const cl = makeClause({pos(p(x_)), neg(p(x_))}); + EXPECT_TRUE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologyVarVsConst) { + // {P(X), ¬P(a)} → NOT tautology (syntactically different) + Clause const cl = makeClause({pos(p(x_)), neg(p(a_))}); + EXPECT_FALSE(isTautology(cl)); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Subsumption Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(SimplifyTest, SubsumesSubset) { + // {P(a)} subsumes {P(a), Q(b)} + Clause const gen = makeClause({pos(p(a_))}); + Clause const spec = makeClause({pos(p(a_)), pos(q(b_))}); + EXPECT_TRUE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesIdentical) { + // {P(a), Q(b)} subsumes {P(a), Q(b)} + Clause const c1 = makeClause({pos(p(a_)), pos(q(b_))}); + Clause const c2 = makeClause({pos(p(a_)), pos(q(b_))}); + EXPECT_TRUE(subsumes(c1, c2)); +} + +TEST_F(SimplifyTest, SubsumesEmptyClause) { + // {} subsumes everything + Clause const empty = makeClause({}); + Clause const cl = makeClause({pos(p(a_)), neg(q(b_))}); + EXPECT_TRUE(subsumes(empty, cl)); +} + +TEST_F(SimplifyTest, SubsumesNotLarger) { + // {P(a), Q(b)} does NOT subsume {P(a)} + Clause const gen = makeClause({pos(p(a_)), pos(q(b_))}); + Clause const spec = makeClause({pos(p(a_))}); + EXPECT_FALSE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesRequiresSamePolarity) { + // {P(a)} does NOT subsume {¬P(a)} + Clause const gen = makeClause({pos(p(a_))}); + Clause const spec = makeClause({neg(p(a_))}); + EXPECT_FALSE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesRequiresSameAtom) { + // {P(a)} does NOT subsume {P(b)} + Clause const gen = makeClause({pos(p(a_))}); + Clause const spec = makeClause({pos(p(b_))}); + EXPECT_FALSE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesNegativeLiterals) { + // {¬P(a)} subsumes {¬P(a), Q(b)} + Clause const gen = makeClause({neg(p(a_))}); + Clause const spec = makeClause({neg(p(a_)), pos(q(b_))}); + EXPECT_TRUE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesOrderIndependent) { + // {Q(b), P(a)} subsumes {P(a), Q(b), R(a,b)} regardless of order + Clause const gen = makeClause({pos(q(b_)), pos(p(a_))}); + Clause const spec = makeClause({pos(p(a_)), pos(q(b_)), pos(r(a_, b_))}); + EXPECT_TRUE(subsumes(gen, spec)); +} + +} // namespace +} // namespace atp diff --git a/proofsearch/tests/test_term_bank.cc b/proofsearch/tests/test_term_bank.cc new file mode 100644 index 0000000..0d4fcc7 --- /dev/null +++ b/proofsearch/tests/test_term_bank.cc @@ -0,0 +1,339 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/literal.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +#include <cstddef> +#include <gtest/gtest.h> +#include <span> +#include <stdexcept> +#include <utility> + +namespace atp { +namespace { + +// ═══════════════════════════════════════════════════════════════════════════ +// SymbolTable Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(SymbolTableTest, InternReturnsConsistentId) { + SymbolTable st; + SymbolId const id1 = st.intern("foo", SymbolKind::kFunction, 2); + SymbolId const id2 = st.intern("foo", SymbolKind::kFunction, 2); + EXPECT_EQ(id1, id2); +} + +TEST(SymbolTableTest, DifferentNamesGetDifferentIds) { + SymbolTable st; + SymbolId const a = st.intern("a", SymbolKind::kConstant); + SymbolId const b = st.intern("b", SymbolKind::kConstant); + EXPECT_NE(a, b); +} + +TEST(SymbolTableTest, GetNameRoundTrips) { + SymbolTable st; + SymbolId const id = st.intern("hello", SymbolKind::kFunction, 1); + EXPECT_EQ(st.getName(id), "hello"); +} + +TEST(SymbolTableTest, GetInfoPreservesMetadata) { + SymbolTable st; + SymbolId const id = st.intern("P", SymbolKind::kPredicate, 3, 42); + const SymbolInfo& info = st.getInfo(id); + EXPECT_EQ(info.name_, "P"); + EXPECT_EQ(info.kind_, SymbolKind::kPredicate); + EXPECT_EQ(info.arity_, 3); + EXPECT_EQ(info.sort_, 42); +} + +TEST(SymbolTableTest, IsVariableDetectsKind) { + SymbolTable st; + SymbolId const var = st.intern("X", SymbolKind::kVariable); + SymbolId const con = st.intern("a", SymbolKind::kConstant); + SymbolId const fun = st.intern("f", SymbolKind::kFunction, 1); + EXPECT_TRUE(st.isVariable(var)); + EXPECT_FALSE(st.isVariable(con)); + EXPECT_FALSE(st.isVariable(fun)); +} + +TEST(SymbolTableTest, MismatchKindThrows) { + SymbolTable st; + st.intern("x", SymbolKind::kConstant); + EXPECT_THROW(st.intern("x", SymbolKind::kVariable), std::runtime_error); +} + +TEST(SymbolTableTest, MismatchArityThrows) { + SymbolTable st; + st.intern("f", SymbolKind::kFunction, 1); + EXPECT_THROW(st.intern("f", SymbolKind::kFunction, 2), std::runtime_error); +} + +TEST(SymbolTableTest, SizeTracksInternedSymbols) { + SymbolTable st; + EXPECT_EQ(st.size(), 0); + st.intern("a", SymbolKind::kConstant); + EXPECT_EQ(st.size(), 1); + st.intern("b", SymbolKind::kConstant); + EXPECT_EQ(st.size(), 2); + st.intern("a", SymbolKind::kConstant); // duplicate + EXPECT_EQ(st.size(), 2); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// TermBank Tests +// ═══════════════════════════════════════════════════════════════════════════ + +class TermBankTest : public ::testing::Test { + protected: + SymbolTable symbols_; + TermBank bank_{symbols_}; + + SymbolId sym_a_{}, sym_b_{}, sym_f_{}, sym_g_{}, sym_x_id_{}, sym_y_id_{}; + + void SetUp() override { + sym_a_ = symbols_.intern("a", SymbolKind::kConstant); + sym_b_ = symbols_.intern("b", SymbolKind::kConstant); + sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1); + sym_g_ = symbols_.intern("g", SymbolKind::kFunction, 2); + sym_x_id_ = symbols_.intern("X", SymbolKind::kVariable); + sym_y_id_ = symbols_.intern("Y", SymbolKind::kVariable); + } +}; + +TEST_F(TermBankTest, HashConsingReturnsSameId) { + const TermId kA1 = bank_.makeTerm(sym_a_, {}); + const TermId kA2 = bank_.makeTerm(sym_a_, {}); + EXPECT_EQ(kA1, kA2) << "Hash consing failed: same term got different IDs"; +} + +TEST_F(TermBankTest, DifferentTermsGetDifferentIds) { + const TermId kA = bank_.makeTerm(sym_a_, {}); + const TermId kB = bank_.makeTerm(sym_b_, {}); + EXPECT_NE(kA, kB); +} + +TEST_F(TermBankTest, CompoundTermHashConsing) { + const TermId kA = bank_.makeTerm(sym_a_, {}); + const TermId kB = bank_.makeTerm(sym_b_, {}); + // f(a) + const TermId kFA1 = bank_.makeTerm(sym_f_, {{kA}}); + const TermId kFA2 = bank_.makeTerm(sym_f_, {{kA}}); + EXPECT_EQ(kFA1, kFA2); + // f(b) != f(a) + const TermId kFB = bank_.makeTerm(sym_f_, {{kB}}); + EXPECT_NE(kFA1, kFB); +} + +TEST_F(TermBankTest, NestedTermHashConsing) { + const TermId kA = bank_.makeTerm(sym_a_, {}); + const TermId kFA = bank_.makeTerm(sym_f_, {{kA}}); + // g(f(a), a) + const TermId kGFAA1 = bank_.makeTerm(sym_g_, {{kFA, kA}}); + const TermId kGFAA2 = bank_.makeTerm(sym_g_, {{kFA, kA}}); + EXPECT_EQ(kGFAA1, kGFAA2); +} + +TEST_F(TermBankTest, GetTermReturnsCorrectSymbol) { + const TermId kA = bank_.makeTerm(sym_a_, {}); + const Term& t = bank_.getTerm(kA); + EXPECT_EQ(t.symbol_id_, sym_a_); + EXPECT_EQ(t.arity(), 0); +} + +TEST_F(TermBankTest, GetTermReturnsCorrectArgs) { + const TermId kA = bank_.makeTerm(sym_a_, {}); + const TermId kB = bank_.makeTerm(sym_b_, {}); + const TermId kGAB = bank_.makeTerm(sym_g_, {{kA, kB}}); + + const Term& t = bank_.getTerm(kGAB); + EXPECT_EQ(t.symbol_id_, sym_g_); + EXPECT_EQ(t.arity(), 2); + ASSERT_EQ(t.args_.size(), 2); + EXPECT_EQ(t.args_[0], kA); + EXPECT_EQ(t.args_[1], kB); +} + +TEST_F(TermBankTest, MakeVarCreatesZeroArityTerm) { + const TermId kX = bank_.makeVar(sym_x_id_); + const Term& t = bank_.getTerm(kX); + EXPECT_EQ(t.symbol_id_, sym_x_id_); + EXPECT_EQ(t.arity(), 0); + EXPECT_TRUE(t.args_.empty()); +} + +TEST_F(TermBankTest, IsVariableDistinguishesFromConstants) { + const TermId kX = bank_.makeVar(sym_x_id_); + const TermId kA = bank_.makeTerm(sym_a_, {}); + + EXPECT_TRUE(bank_.isVariable(kX)) << "Variable should be detected as variable"; + EXPECT_FALSE(bank_.isVariable(kA)) << "Constant should NOT be detected as variable"; +} + +TEST_F(TermBankTest, VariableHashConsing) { + const TermId kX1 = bank_.makeVar(sym_x_id_); + const TermId kX2 = bank_.makeVar(sym_x_id_); + EXPECT_EQ(kX1, kX2); + + const TermId kY = bank_.makeVar(sym_y_id_); + EXPECT_NE(kX1, kY); +} + +TEST_F(TermBankTest, SizeTracksUniqueTerms) { + EXPECT_EQ(bank_.size(), 0); + const TermId kA = bank_.makeTerm(sym_a_, {}); + EXPECT_EQ(bank_.size(), 1); + bank_.makeTerm(sym_a_, {}); // duplicate + EXPECT_EQ(bank_.size(), 1); + bank_.makeTerm(sym_b_, {}); + EXPECT_EQ(bank_.size(), 2); + bank_.makeTerm(sym_f_, {{kA}}); + EXPECT_EQ(bank_.size(), 3); +} + +TEST_F(TermBankTest, CompoundTermWithVariableArgs) { + // f(X) — a function applied to a variable + const TermId kX = bank_.makeVar(sym_x_id_); + const TermId kFX = bank_.makeTerm(sym_f_, {{kX}}); + + const Term& t = bank_.getTerm(kFX); + EXPECT_EQ(t.symbol_id_, sym_f_); + EXPECT_EQ(t.arity(), 1); + EXPECT_EQ(t.args_[0], kX); + + EXPECT_FALSE(bank_.isVariable(kFX)); + EXPECT_TRUE(bank_.isVariable(kX)); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// ClauseStore Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(ClauseStoreTest, AddAndRetrieve) { + ClauseStore store; + Clause c; + c.literals_.push_back(Literal{.atom_ = 0, .is_positive_ = true}); + c.literals_.push_back(Literal{.atom_ = 1, .is_positive_ = false}); + + const ClauseId kId = store.addClause(std::move(c)); + EXPECT_EQ(kId, 0); + + const Clause& retrieved = store.getClause(kId); + EXPECT_EQ(retrieved.id_, kId); + EXPECT_EQ(retrieved.literals_.size(), 2); + EXPECT_EQ(retrieved.literals_[0].atom_, 0); + EXPECT_TRUE(retrieved.literals_[0].is_positive_); + EXPECT_EQ(retrieved.literals_[1].atom_, 1); + EXPECT_FALSE(retrieved.literals_[1].is_positive_); +} + +TEST(ClauseStoreTest, AssignsSequentialIds) { + ClauseStore store; + const ClauseId kId0 = store.addClause(Clause{}); + const ClauseId kId1 = store.addClause(Clause{}); + const ClauseId kId2 = store.addClause(Clause{}); + EXPECT_EQ(kId0, 0); + EXPECT_EQ(kId1, 1); + EXPECT_EQ(kId2, 2); + EXPECT_EQ(store.size(), 3); +} + +TEST(ClauseStoreTest, StampsClauseWithId) { + ClauseStore store; + Clause c; + c.id_ = kInvalidId; // unset + const ClauseId kId = store.addClause(std::move(c)); + EXPECT_EQ(store.getClause(kId).id_, kId); +} + +TEST(ClauseStoreTest, MutableAccess) { + ClauseStore store; + Clause c; + c.depth_ = 0; + const ClauseId kId = store.addClause(std::move(c)); + + store.getMutableClause(kId).depth_ = 42; + EXPECT_EQ(store.getClause(kId).depth_, 42); +} + +TEST(ClauseStoreTest, ForEachVisitsAll) { + ClauseStore store; + store.addClause(Clause{}); + store.addClause(Clause{}); + store.addClause(Clause{}); + + size_t count = 0; + store.forEach([&count](const Clause&) { count++; }); + EXPECT_EQ(count, 3); +} + +TEST(ClauseStoreTest, EmptyClauseDetection) { + Clause c; + EXPECT_TRUE(c.isEmpty()); + c.literals_.push_back(Literal{.atom_ = 0, .is_positive_ = true}); + EXPECT_FALSE(c.isEmpty()); + EXPECT_EQ(c.size(), 1); +} + +TEST(ClauseStoreTest, ProvenancePreserved) { + ClauseStore store; + Clause c; + c.rule_ = InferenceRule::kResolution; + c.parent1_ = 3; + c.parent2_ = 7; + c.depth_ = 5; + + ClauseId const id = store.addClause(std::move(c)); + const Clause& retrieved = store.getClause(id); + EXPECT_EQ(retrieved.rule_, InferenceRule::kResolution); + EXPECT_EQ(retrieved.parent1_, 3); + EXPECT_EQ(retrieved.parent2_, 7); + EXPECT_EQ(retrieved.depth_, 5); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Literal Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(LiteralTest, Complement) { + const Literal kPos{.atom_ = 42, .is_positive_ = true}; + const Literal kNeg = kPos.complement(); + EXPECT_EQ(kNeg.atom_, 42); + EXPECT_FALSE(kNeg.is_positive_); + + const Literal kBack = kNeg.complement(); + EXPECT_EQ(kBack, kPos); +} + +TEST(LiteralTest, Equality) { + const Literal kA{.atom_ = 1, .is_positive_ = true}; + const Literal kB{.atom_ = 1, .is_positive_ = true}; + const Literal kC{.atom_ = 1, .is_positive_ = false}; + const Literal kD{.atom_ = 2, .is_positive_ = true}; + EXPECT_EQ(kA, kB); + EXPECT_NE(kA, kC); + EXPECT_NE(kA, kD); +} + +} // namespace +} // namespace atp diff --git a/proofsearch/tests/test_unification.cc b/proofsearch/tests/test_unification.cc new file mode 100644 index 0000000..63ac9f0 --- /dev/null +++ b/proofsearch/tests/test_unification.cc @@ -0,0 +1,355 @@ +/* + * richard-atp-engine: A saturation-based automated theorem prover for first-order logic. + * Copyright (C) 2026 Richard Qin + * + * 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 <https://www.gnu.org/licenses/>. + */ + +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/infer/substitution.h" +#include "atp/infer/unification.h" + +#include <gtest/gtest.h> + +namespace atp { +namespace { + +// ═══════════════════════════════════════════════════════════════════════════ +// Test Fixture +// ═══════════════════════════════════════════════════════════════════════════ + +class UnificationTest : public ::testing::Test { + protected: + SymbolTable symbols_; + TermBank bank_{symbols_}; + + // Symbols + SymbolId sym_a_{}, sym_b_{}, sym_c_{}; + SymbolId sym_f_{}, sym_g_{}, sym_h_{}; + SymbolId sym_p_{}; + SymbolId sym_x_{}, sym_y_{}, sym_z_{}; + + // Terms (created in SetUp) + TermId a_{}, b_{}, c_{}; + TermId x_{}, y_{}, z_{}; + + void SetUp() override { + sym_a_ = symbols_.intern("a", SymbolKind::kConstant); + sym_b_ = symbols_.intern("b", SymbolKind::kConstant); + sym_c_ = symbols_.intern("c", SymbolKind::kConstant); + sym_f_ = symbols_.intern("f", SymbolKind::kFunction, 1); + sym_g_ = symbols_.intern("g", SymbolKind::kFunction, 2); + sym_h_ = symbols_.intern("h", SymbolKind::kFunction, 1); + sym_p_ = symbols_.intern("P", SymbolKind::kPredicate, 2); + sym_x_ = symbols_.intern("X", SymbolKind::kVariable); + sym_y_ = symbols_.intern("Y", SymbolKind::kVariable); + sym_z_ = symbols_.intern("Z", SymbolKind::kVariable); + + a_ = bank_.makeTerm(sym_a_, {}); + b_ = bank_.makeTerm(sym_b_, {}); + c_ = bank_.makeTerm(sym_c_, {}); + x_ = bank_.makeVar(sym_x_); + y_ = bank_.makeVar(sym_y_); + z_ = bank_.makeVar(sym_z_); + } + + // Helper: make f(arg) + TermId f(TermId arg) { return bank_.makeTerm(sym_f_, {{arg}}); } + // Helper: make g(arg1, arg2) + TermId g(TermId a1, TermId a2) { return bank_.makeTerm(sym_g_, {{a1, a2}}); } + // Helper: make h(arg) + TermId h(TermId arg) { return bank_.makeTerm(sym_h_, {{arg}}); } + // Helper: make P(arg1, arg2) + TermId p(TermId a1, TermId a2) { return bank_.makeTerm(sym_p_, {{a1, a2}}); } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// Substitution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, SubstBindAndLookup) { + Substitution subst; + EXPECT_TRUE(subst.bind(x_, a_)); + EXPECT_EQ(subst.lookup(x_), a_); + EXPECT_EQ(subst.lookup(y_), kInvalidId); // unbound +} + +TEST_F(UnificationTest, SubstBindSameTermSucceeds) { + Substitution subst; + EXPECT_TRUE(subst.bind(x_, a_)); + EXPECT_TRUE(subst.bind(x_, a_)); // same binding → OK +} + +TEST_F(UnificationTest, SubstBindDifferentTermFails) { + Substitution subst; + EXPECT_TRUE(subst.bind(x_, a_)); + EXPECT_FALSE(subst.bind(x_, b_)); // different binding → fail +} + +TEST_F(UnificationTest, SubstResolveChain) { + // X → Y → a + Substitution subst; + subst.bind(x_, y_); + subst.bind(y_, a_); + EXPECT_EQ(subst.resolve(x_, bank_), a_); +} + +TEST_F(UnificationTest, SubstResolveUnbound) { + Substitution const subst; + EXPECT_EQ(subst.resolve(x_, bank_), x_); // unbound → returns itself +} + +TEST_F(UnificationTest, SubstResolveNonVariable) { + Substitution const subst; + EXPECT_EQ(subst.resolve(a_, bank_), a_); // constant → returns itself +} + +TEST_F(UnificationTest, SubstApplySimple) { + // σ = {X → a} apply to f(X) → f(a) + Substitution subst; + subst.bind(x_, a_); + TermId const fx = f(x_); + TermId const result = subst.apply(fx, bank_); + TermId const expected = f(a_); + EXPECT_EQ(result, expected); +} + +TEST_F(UnificationTest, SubstApplyLeavesUnbound) { + // σ = {X → a} apply to g(X, Y) → g(a, Y) + Substitution subst; + subst.bind(x_, a_); + TermId const gxy = g(x_, y_); + TermId const result = subst.apply(gxy, bank_); + TermId const expected = g(a_, y_); + EXPECT_EQ(result, expected); +} + +TEST_F(UnificationTest, SubstApplyNested) { + // σ = {X → f(a)} apply to g(X, b) → g(f(a), b) + Substitution subst; + subst.bind(x_, f(a_)); + TermId const result = subst.apply(g(x_, b_), bank_); + EXPECT_EQ(result, g(f(a_), b_)); +} + +TEST_F(UnificationTest, SubstOccursIn) { + Substitution const subst; + // X occurs in f(X) + EXPECT_TRUE(subst.occursIn(x_, f(x_), bank_)); + // X occurs in g(a, f(X)) + EXPECT_TRUE(subst.occursIn(x_, g(a_, f(x_)), bank_)); + // X does NOT occur in f(a) + EXPECT_FALSE(subst.occursIn(x_, f(a_), bank_)); + // X does NOT occur in Y (different variable) + EXPECT_FALSE(subst.occursIn(x_, y_, bank_)); +} + +TEST_F(UnificationTest, SubstClearAndSize) { + Substitution subst; + EXPECT_TRUE(subst.empty()); + subst.bind(x_, a_); + subst.bind(y_, b_); + EXPECT_EQ(subst.size(), 2); + subst.clear(); + EXPECT_TRUE(subst.empty()); + EXPECT_EQ(subst.lookup(x_), kInvalidId); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Unification Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, UnifyIdenticalConstants) { + Substitution subst; + EXPECT_TRUE(unify(bank_, a_, a_, subst)); + EXPECT_TRUE(subst.empty()); +} + +TEST_F(UnificationTest, UnifyDifferentConstants) { + Substitution subst; + EXPECT_FALSE(unify(bank_, a_, b_, subst)); +} + +TEST_F(UnificationTest, UnifyVarWithConstant) { + Substitution subst; + EXPECT_TRUE(unify(bank_, x_, a_, subst)); + EXPECT_EQ(subst.resolve(x_, bank_), a_); +} + +TEST_F(UnificationTest, UnifyConstantWithVar) { + // Symmetric: unify(a, X) should also work + Substitution subst; + EXPECT_TRUE(unify(bank_, a_, x_, subst)); + EXPECT_EQ(subst.resolve(x_, bank_), a_); +} + +TEST_F(UnificationTest, UnifyTwoVariables) { + Substitution subst; + EXPECT_TRUE(unify(bank_, x_, y_, subst)); + // One should be bound to the other + TermId const rx = subst.resolve(x_, bank_); + TermId const ry = subst.resolve(y_, bank_); + EXPECT_EQ(rx, ry); +} + +TEST_F(UnificationTest, UnifyCompoundTerms) { + // f(X) =? f(a) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank_, f(x_), f(a_), subst)); + EXPECT_EQ(subst.resolve(x_, bank_), a_); +} + +TEST_F(UnificationTest, UnifyMultipleArgs) { + // g(X, Y) =? g(a, b) → {X → a, Y → b} + Substitution subst; + EXPECT_TRUE(unify(bank_, g(x_, y_), g(a_, b_), subst)); + EXPECT_EQ(subst.resolve(x_, bank_), a_); + EXPECT_EQ(subst.resolve(y_, bank_), b_); +} + +TEST_F(UnificationTest, UnifyConflictingBindings) { + // g(X, X) =? g(a, b) → fails (X can't be both a and b) + Substitution subst; + EXPECT_FALSE(unify(bank_, g(x_, x_), g(a_, b_), subst)); +} + +TEST_F(UnificationTest, UnifyConsistentRepeatedVar) { + // g(X, X) =? g(a, a) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank_, g(x_, x_), g(a_, a_), subst)); + EXPECT_EQ(subst.resolve(x_, bank_), a_); +} + +TEST_F(UnificationTest, UnifyDifferentHeadSymbols) { + // f(X) =? h(X) → fails + Substitution subst; + EXPECT_FALSE(unify(bank_, f(x_), h(x_), subst)); +} + +TEST_F(UnificationTest, UnifyDifferentArity) { + // f(X) =? g(X, Y) → fails (arity 1 vs 2) + Substitution subst; + EXPECT_FALSE(unify(bank_, f(x_), g(x_, y_), subst)); +} + +TEST_F(UnificationTest, UnifyNestedTerms) { + // f(g(X, a)) =? f(Y) → {Y → g(X, a)} + Substitution subst; + EXPECT_TRUE(unify(bank_, f(g(x_, a_)), f(y_), subst)); + EXPECT_EQ(subst.resolve(y_, bank_), g(x_, a_)); +} + +TEST_F(UnificationTest, UnifyVarWithCompound) { + // X =? f(a) → {X → f(a)} + Substitution subst; + EXPECT_TRUE(unify(bank_, x_, f(a_), subst)); + EXPECT_EQ(subst.resolve(x_, bank_), f(a_)); +} + +TEST_F(UnificationTest, UnifyDeepNesting) { + // f(f(f(X))) =? f(f(f(a))) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank_, f(f(f(x_))), f(f(f(a_))), subst)); + EXPECT_EQ(subst.resolve(x_, bank_), a_); +} + +TEST_F(UnificationTest, UnifyChainedVariables) { + // g(X, Y) =? g(Y, a) → {X → Y, Y → a} effectively X → a + Substitution subst; + EXPECT_TRUE(unify(bank_, g(x_, y_), g(y_, a_), subst)); + EXPECT_EQ(subst.resolve(x_, bank_), a_); + EXPECT_EQ(subst.resolve(y_, bank_), a_); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Occurs Check Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, OccursCheckBlocks) { + // X =? f(X) with occurs check → fails + Substitution subst; + UnificationConfig const config{.enable_occurs_check_ = true}; + EXPECT_FALSE(unify(bank_, x_, f(x_), subst, config)); +} + +TEST_F(UnificationTest, OccursCheckDisabledAllows) { + // X =? f(X) without occurs check → succeeds (unsound but fast) + Substitution subst; + UnificationConfig const config{.enable_occurs_check_ = false}; + EXPECT_TRUE(unify(bank_, x_, f(x_), subst, config)); +} + +TEST_F(UnificationTest, OccursCheckDeep) { + // X =? f(g(X, a)) with occurs check → fails + Substitution subst; + UnificationConfig const config{.enable_occurs_check_ = true}; + EXPECT_FALSE(unify(bank_, x_, f(g(x_, a_)), subst, config)); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// applySubstitution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, ApplySubstitutionSimple) { + Substitution subst; + subst.bind(x_, a_); + EXPECT_EQ(applySubstitution(subst, f(x_), bank_), f(a_)); +} + +TEST_F(UnificationTest, ApplySubstitutionNested) { + Substitution subst; + subst.bind(x_, a_); + subst.bind(y_, b_); + EXPECT_EQ(applySubstitution(subst, g(f(x_), y_), bank_), g(f(a_), b_)); +} + +TEST_F(UnificationTest, ApplySubstitutionPreservesUnbound) { + Substitution subst; + subst.bind(x_, a_); + // Y is unbound → stays as Y + EXPECT_EQ(applySubstitution(subst, g(x_, y_), bank_), g(a_, y_)); +} + +TEST_F(UnificationTest, ApplySubstitutionToConstant) { + Substitution subst; + subst.bind(x_, a_); + // Constant is unchanged + EXPECT_EQ(applySubstitution(subst, b_, bank_), b_); +} + +TEST_F(UnificationTest, ApplySubstitutionChain) { + // σ = {X → Y, Y → a} apply to f(X) → f(a) + Substitution subst; + subst.bind(x_, y_); + subst.bind(y_, a_); + EXPECT_EQ(applySubstitution(subst, f(x_), bank_), f(a_)); +} + +TEST_F(UnificationTest, UnifyThenApply) { + // Full round-trip: unify P(X, f(Y)) with P(a, f(b)), then apply + Substitution subst; + TermId const lhs = p(x_, f(y_)); + TermId const rhs = p(a_, f(b_)); + ASSERT_TRUE(unify(bank_, lhs, rhs, subst)); + + EXPECT_EQ(applySubstitution(subst, lhs, bank_), p(a_, f(b_))); + EXPECT_EQ(applySubstitution(subst, rhs, bank_), p(a_, f(b_))); + // Both sides should produce the same term after applying the MGU + EXPECT_EQ(applySubstitution(subst, lhs, bank_), applySubstitution(subst, rhs, bank_)); +} + +} // namespace +} // namespace atp |