Abstract
We discuss a sequent style clause-based proof system that supports several important strategies in automatic theorem proving. The system has a goal-subgoal structure and supports back chaining with caching; it permits semantic deletion, sometimes using multiple models; it is also a genuine set of support strategy; and it is complete for first order logic in clause form.
Cite
CITATION STYLE
Nie, X., & Plaisted, D. A. (1990). A complete semantic back chaining proof system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 449 LNAI, pp. 16–27). Springer Verlag. https://doi.org/10.1007/3-540-52885-7_76
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
