Deciding Clause Classes by Semantic Clash Resolution

Article type: Research Article

Authors: Leitsch, Alexander

Affiliations: Institute für Computersprachen, Technical University of Vienna, Resselgasse 3, 1040 Wien, Austria

Abstract: It is investigated, how semantic clash resolution can be used to decide some classes of clause sets. Because semantic clash resolution is complete, the termination of the resolution procedure on a class Γ gives a decision procedure for Γ. Besides generalizing earlier results we investigate the relation between termination and clause complexity. For this purpose we define the general concept of atom complexity measure and show some general results about termination in terms of such measures. Moreover, rather than using fixed resolution refinements we define an algorithmic generator for decision procedures, which constructs appropriate semantic refinements out of the syntactical structure of the clause sets. This method is applied to the Bernays – Schönfinkel class, where it gives an efficient (resolution) decision procedure.

DOI: 10.3233/FI-1993-182-406

Journal: Fundamenta Informaticae, vol. 18, no. 2-4, pp. 163-182, 1993