| Autor: |
Leidinger, Hendrik, Weidenbach, Christoph |
| Rok vydání: |
2022 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
We propose a new calculus SCL(EQ) for first-order logic with equality that only learns non-redundant clauses. Following the idea of CDCL (Conflict Driven Clause Learning) and SCL (Clause Learning from Simple Models) a ground literal model assumption is used to guide inferences that are then guaranteed to be non-redundant. Redundancy is defined with respect to a dynamically changing ordering derived from the ground literal model assumption. We prove SCL(EQ) sound and complete and provide examples where our calculus improves on superposition. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
