diff options
| author | Richard Qin <richard.qin.x@gmail.com> | 2026-04-03 14:21:40 +0800 |
|---|---|---|
| committer | Richard Qin <richard.qin.x@gmail.com> | 2026-04-03 14:21:40 +0800 |
| commit | df6c2f124fce4cecd42da806a003afdf3a922c09 (patch) | |
| tree | 9578ecd7b2585d164970366bf6f45cb37f8c4cf3 /proofsearch/CMakeLists.txt | |
| parent | 52ff8a1695a2cc5157b98d4e71b05d7ea58bb97a (diff) | |
| download | rcc-project-df6c2f124fce4cecd42da806a003afdf3a922c09.tar.gz rcc-project-df6c2f124fce4cecd42da806a003afdf3a922c09.tar.xz | |
feat: implement substitution logic and unify/applySubstitution functions for term resolution
Diffstat (limited to 'proofsearch/CMakeLists.txt')
| -rw-r--r-- | proofsearch/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofsearch/CMakeLists.txt b/proofsearch/CMakeLists.txt index 2cf69db..edeb6b7 100644 --- a/proofsearch/CMakeLists.txt +++ b/proofsearch/CMakeLists.txt @@ -72,6 +72,7 @@ set(ATP_SOURCES 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 |