×

Automatisches Theorembeweisen mit Konfigurationen. (Automatic theorem proving with configurations). (German) Zbl 0586.68076

The present paper represents a new non-resolution approach based on the explicit development of interpretations on clause sets. The main concept - configurations - represent classes of pseudo-semantic trees from resolution theory [C. L. Chang and R. C. Lee: Symbolic logic and mechanical theorem proving (1973; Zbl 0263.68046)]. The semantics of configurations is obtained by relating them to first-order logical expressions. As inference operations on configurations are defined: reduction (a subgoal to be solved is identified with already solved subgoals and disactivated) and expansion (introducing new subgoals to be solved). The inference rules are investigated on the most interesting configuration types. These methods are formulated in terms of refutation procedures, the non-satisfiability being translated into (potential) contradictory sets of axioms. The correctness and completeness properties are underlined and many results from resolution strategies or Horn clause sets are obtained as special cases. Methods to minimize the search space are obtained and analyzed by conditioning the literal-selection function, the inference rules, the configuration types. The configurations can be viewed not only as a base for the development of new methods but also as a very suitable concept to compare and to better understand other different methods in theorem proving.
Reviewer: N.Curteanu

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Citations:

Zbl 0263.68046
PDFBibTeX XMLCite