ISSN:
1436-5057
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Description / Table of Contents:
Summary Starting from a special formulation of first order functional calculus two procedures are presented producing refutations of inconsistent formulas. Both procedures are based on the notion of interconnecting literals. The first one goes back toHerbrand's Theorem. LetF n be the conjunction ofn copies of the formulaF. An algorithm is introduced to decide whether, for a fixedn, there is an assignment β for the variables ofF n making the formula βF n completely interconnected. By applying this algorithm forn=1,2,... a truth-functionally inconsistent formula of minimal length is constructed. The basic idea of the second procedure is to produce fromF new oneliteral clauses (which are consisten withF). In many cases this proofprocedure, while not complete, is very effective in comparison with other programs; some examples of machine-refutations are given in the appendix. The method may be generalized; in particular it suggests a possibility of man-machine interaction in theorem-proving.
Notes:
Zusammenfassung Ausgehend von einer speziellen Formulierung des Prädikatenkalküls 1. Stufe werden zwei Verfahren entwickelt, welche Widerlegungen inkonsistenter FormelnF liefern. Grundlegend für beide Verfahren ist der Begriff der Verkettung von Literals. Das erste beruht auf demHerbrad-Theorem. SeiF n die Konjunktion vonn Exemplaren der FormelF. Es wird ein Algorithmus angegeben, der entscheidet, ob es bei gegebenemn eine Belegung β der Variablen vonF n gibt, bei welcher die Formel βF n vollständig verkettet ist. Die Anwendung dieses Algorithmus fürn=1,2, ... führt zur Konstruktion einer aussagenlogisch inkonsistenten Formel minimaler Länge. Das zweite Verfahren beruht darauf, daß neue Clausen erzeugt werden, die aus nur einem Literal bestehen (und die mitF konsistent sind). Dieses Verfahren ist nicht vollständig, liefert aber in vielen Fällen schnellere Widerlegungen als andere Methoden; einige Maschinen-Protokolle solcher Widerlegungen sind im Anhang zusammengestellt. Das Verfahren läßt sich verallgemeinern; insbesondere bietet es eine Möglichkeit des Zusammenwirkens von Mensch und Maschine beim Beweisen mathematischer Sätze.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF02236612
Permalink