Abstract
There are automated reasoning building blocks shared between the prime calculi for propositional and first-order logic with equality, conflict driven clause learning (CDCL) and superposition, respectively. In this paper I identify these building blocks by a projection of superposition to propositional logic. Underlying both calculi is a partial model assumption guiding ordered resolution inferences that are not redundant.
Cite
CITATION STYLE
Weidenbach, C. (2015). Automated reasoning building blocks. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9360 LNCS, pp. 172–188). Springer Verlag. https://doi.org/10.1007/978-3-319-23506-6_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
