A semantic backward chaining proof system

摘要

We discuss a refutationally complete sequent style clause-based proof system that supports several important strategies in automatic theorem proving. The system has a goal-subgoal structure and supports backward chaining with caching. It permits semantic deletion, sometimes using multiple interpretations. It is also a genuine support strategy. We also show how to use multiple interpretations to control the case analysis rule, also called the splitting rule, how to design interpretations and how to select input clauses for a theorem.