LITERATUUR



Formele logica: Resolutie.



@

R. Anderson, W.W. Bledsoe

(1970):
A linear format for resolution with merging and a new technique for establishing completeness.
In: ' Journal of the ACM ' 17(3), 525-534 (1970).

@

W. Ackermann

(1928):
Über die Erfüllbarkeit gewisser Zählausdrücke.
In: ' Mathematische Annalen ' 100, 638-649 (1928).

@

A. Aho, J. Hopcroft, J. Ullman

(1975):
The design and analysis of computer algorithms.
Addison-Wesley (1975).

@

P.B. Andrews

(1981):
Theorem proving via general matings.
In: ' Journal of the ACM ' 28(2), 193-214 (1981).

@

M. Baaz

(1987):
Automatisches Beweisen für Logiksysteme, in denen Widersprüche behandelt werden können.
In: ' Informatik-Fachberichte ' 151.
Springer, 1987.

@

M. Baaz, C. Fermüller, A. Leitsch

(1994):
A non-elementary speed-up in proof length by structural clause form transformation.
In: ' Proceedings LICS '94 ',
IEEE Computer Science Press, 213-219 (1994).

@

A. Barr, E.A. Feigenbaum (eds.)

(1981):
The handbook of Artificial Intelligence, vol. I, chap. 2, "Search".
Pitman Books (1981).

@

L. Bachmair, H. Ganzinger

(1994):
Rewrite-based equational theorem proving with selection and simplification.
In: ' Journal of Logic and Computation ' 4(3), 1-31 (1994).

@

W. Bibel

(1982):
Automated theorem proving.
Vieweg (1982).

@

G.S. Boolos, R.C. Jeffrey

(1974):
Computability and logic.
Cambridge University Press (1974).

@

W.S. Brainerd, L.H. Landweber

(1974):
Theory of computation.
John Wiley & Sons (1974)

@

M. Baaz, A. Leitsch

(1985):
Die Anwendung starker Reduktionsregeln im automatischen Beweisen.
In: ' Proc. of the Austrian Academy of Sciences ' II 194(4-10), 287-307 (1985).

@

M. Baaz, A. Leitsch

(1990):
A strong reduction method based on function in production,
In: ' ISSAC'90 ', ACM Press 30-37 (1990).

@

M. Baaz, A. Leitsch

(1992):
Complexity of resolution proofs and function introduction.
In: ' Annals of Pure and Applied Logic ' 57, 181-215 (1992).

@

M. Baaz, A. Leitsch

(1994):
On skolemization and proof complexity.
In: ' Fundamenta Informaticae ' 20 (4), 353-379 (1994).

@

E. Börger

(1992):
Berechenbarkeit, Komplexität, Logik.
Vieweg (1992).

@

R.S. Boyer

(1971):
Locking: a restriction of resolution.
The University of Texas at Austin,
Ph.D. dissertation (1971).

@

P. Bernays, M. Schönfinkel

(1928):
Zum Entscheidungsproblem der Mathematischen Logik.
In: ' Math. Annalen ' 99, 342-372 (1928).

@

T. Boy de la Tour

(1990):
Minimizing the number of clauses by renaming.
In: ' Proc. LADE ' 10, 558-572.
Springer (1990)

@

C.L. Chang

(1972):
Theorem proving with variable-constraint resolution.
In: ' Information Sciences ' 4, 217-231.

@

A. Church

(1936):
A note on the Entscheidungsproblem.
In: ' Journal of Symbolic Logic ' 1, 40-44 (1936).

@

S. Ceri, G. Gottlob, L. Tanca

(1990):
Logic programming and databases.
Springer (1990).

@

C.L. Chang, R.C.T. Lee

(1973):
Symbolic logic and mechanical theorem proving.
Academic Press (1973).

@

R. Caferra, N. Peltier

(1996):
Decision procedures using model building techniques.
Proc. CSL,
In: ' Lecture Notes in Computer Science ' 1092, 130-144,
Springer (1996)

@

R. Caferra, N. Zabel

(1992):
A method for simultaneous search for refutations and models by equational constraint solving.
In: ' Journal of Symbolic Computation ' 13, 613-641 (1992).

@

M. Davis, G. Logemann, D. Loveland

(1962):
A machine program for theorem proving.
In: ' Communications of the ACM ' 5 (7), 394-397 (1962).

@

M. Davis, H. Putnam

(1960):
A computing procedure for quantification theory.
In: ' Journal of the ACM ' 7 (3), 201-215 (1960).

@

L. Denenberg, H.R. Lewis

(1984):
'Logical syntax and computational complexity '.
In: ' Lecture Notes in Math. ' 1104, 101-115,
Springer (1984).

@

E. Eder

(1985):
Properties of substitutions and unifications.
In: ' J. Symbolic Computation ' 1, 31-46 (1985).

@

E. Eder

(1992):
Relative complexities of first-order calculi,
Vieweg (1992).

@

U. Egly

(1990):
Problem reduction methods and clause splitting in automated theorem proving.
Master thesis,
Technische Universität Wien (1990).

@

U. Egly

(1991):
A generalized factorization rule based on the introduction of Skolem terms.
In: ' Proc. Seventh Austrian Conference on Artificial Intelligence ', 'Informatik-Fachberichte ' 287,
Springer (1991)

@

U. Egly

(1992):
Shortening proofs by quantifier introduction.
Proc. LPAR'92,
In: ' Lecture Notes in AI ' 624, 148-159,
Springer (1992).

@

U. Egly

(1994):
Methods of function introduction.
Dissertation, TU Darmstadt (1994).

@

C. Fermüller

(1991):
Deciding classes of clause sets by resolution.
Dissertation, Technische Universitüt Wien (1991).

@

C. Fermüller

(1991):
A resolution variant deciding some classes of clause sets.
Proc. CSL '90,
In: ' Lecture Notes in Computer Science ' 533, 128-144,
Springer (1991).

@

M.C. Fitting

(1990):
First-order logic and automated theorem proving.
Springer (1990).

@

C. Fermüller, A. Leitsch

(1993):
Model building by resolution.
Proc. CSL '92,
In: ' Lecture Notes in Computer Science ' 702, 134-148,
Springer (1993).

@

C. Fermüller, A. Leitsch

(1996):
Hyperresolution and automated model building.
In: ' Journal of Logic and Computation ' 6 (2), 173-203 (1996).

@

C. Fermüller, A. Leitsch, T. Tammet, N. Zamov

(1993):
Resolution methods for the decision problem.
In: ' Lecture Notes in AI ' 679,
Springer (1993).

@

G.Gentzen

(1934):
Untersuchungen über das logische Schliessen I-II.
In: ' Math. Z. ' 39, 176-210, 405-431 (1934).

@

G. Gottlob, Ch. Fermüller

(1993):
Removing redundancy from a clause.
In: ' Artificial Intelligence ' 61, 263-289 (1993).

@

D.M. Gabbay, C.J. Hogger (eds.) (19..):


Handbook of logic in artificial intelligence and logic programming.
Oxford University Press (1993).

@

P.C. Gilmore

(1960):
A proof method for quantification theory; its justification and realization.
In: ' IBM J. Res. Develop. ' 4, 28-35 (1960).

@

M.R. Garey, D.S. Johnson

(1979):
Computers and intractability.
Freeman (1979).

@

G. Gottlob, A. Leitsch

(1985):
On the efficiency of subsumption algorithms.
In: ' Journal of the ACM ' 32 (2), 280-295 (1985).

@

G. Gottlob, A. Leitsch

(1985):
Fast subsumption algorithms.
Proc. EUROCAL '85,
In: ' Lecture Notes in Computer Science ' 204-II, 64-77,
Springer (1985). K. Gödel (1930):
Die Vollständigkeit der Axiome des logischen Funktionenkalküls.
In: ' Mh. Math. Phys. ' 37, 349-360 (1930).

@

K. Gödel

(1931):
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme.
In: ' Mh. Math. Phys. ' 38, 175-198 (1931).

@

K. Gödel

(1932):
Ein Spezialfall des Entscheidungsproblems der theoretischen Logik.
In: ' Ergebn. math. Kolloq. ' 2, 27-28 (1932).

@

G. Gottlob

(1987):
Subsumption and implication.
In: ' Information Processing Letters ' 24, 109-111 (1987).

@

Y. Gurevich

(1973):
Formuly s odnim <img src="al2img_l\qnu1bl.gif"> (formulas with one <img src="al2img_l\qnu1bl.gif">).
In: ' Izbrannye voprosy algebry i logiki ' (Selected Questions in Algebra and Logics; in memory of A. Mal'cev).
Nauka, Nowosibirsk, 97-110 (1973).

@

D. Hilbert, P. Bernays

(1934, 1970):
Grundlagen der Mathematik II,
Springer (1970).

@

J. Herbrand

(1930):
Recherches sur la theorie de la démonstration.
In: ' Travaux de la Societé des Sciences et des Lettres de Varsovie ' 33 (1930).

@

J. Herbrand

(1931):
Sur le problème fondamentale de la logique mathématique.
Sprawozdania z posiedzen' Towarzystwa Naukowego Warzawskiego.
In: ' Wydzial III ', 33 (1931).

@

D. Hilbert

(1901):
Probleme der Mathematik.
In: ' Archiv der Mathematik und Physik 3 ' (1), 44-63, 213-237 (1901).

@

R. Imhoff

(1985):
Subsumptionsalgorithmen und ihre Effizienz.
Master's thesis.
Dept. of Mathematics, Univ. of Linz Austria (1985).

@

W.H. Joyner

(1973):
Automated theorem proving and the decision problem.
Ph.D. thesis,
Harvard University (1973).

@

W.H. Joyner

(1976):
Resolution strategies as decision procedures.
In: ' Journal of the ACM ' 23(1), 398-417 (1976).

@

D.E. Knuth

(1968):
The art of computer programming.
Addison-Wesley (1968).

@

S. Klingenbeck, R. Hähnle

(1994):
Semantic tableaus with ordering restrictions.
Proc. of the CADE '94,
In: ' Lecture Notes in AI ' 814, 708-722,
Springer (1994).

@

R. Kowalski, P. Hayes

(1969):
Semantic trees in automatic theorem proving.
In: B. Meltzer, D. Michie (eds.) (1969): 'Machine Intelligence ' 4, 87-101,
Elsevier (1969).

@

R. Kowalski

(1975):
A proof procedure using connection graphs.
In: Journal of the ACM ' 22, 572-595 (1975). '

@

J. Krajicek, P. Pudlak

(1988):
The number of proof lines and the size of proofs in first-order logic.
In: ' Arch. Math. Logic ' 27, 69-84 (1988).

@

A.S. Kahr, E.F. Moore, Hao Wang

(1962):
Entscheidungsproblem reduced to the <img src="al2img_l\qnu1bl.gif"> <img src="al2img_l\qnx1bl.gif"> <img src="al2img_l\qnu1bl.gif"> case.
In: ' Proc. Nat. Acad. Sci. USA ' 48, 365-377 (1962).

@

R.C.T. Lee

(1967):
A completeness theorem and a computer program for finding theorems derivable from given axioms.
Ph.D. thesis,
University of California at Berkeley (1967).

@

G.W. Leibniz

(1923):
Calculus ratiocinator.
In (1923): 'Sämtliche Schriften und Briefe edited by Preussische Akademie der Wissenschaften Darmstadt ',
Reichel (1923).

@

A. Leitsch

(1988):
Implication algorithms for classes of Horn clauses.
In: W.H. Janko (ed.): 'Statistik Informatik + Okonomie ' 172-189,
Springer (1988).

@

A. Leitsch

(1989):
On different concepts of resolution.
In: ' Zeitschr. für Math. Logik und Grundlagen der Math. ' 35, 71-77 (1989).

@

A. Leitsch

(1990):
Deciding Horn classes by hyperresolution.
Proc. of the CSL '89,
In: ' Lecture Notes in Computer Science ' 440, 225-241,
Springer (1990)

@

A. Leitsch

(1993):
Deciding clause classes by semantic clash resolution.
In: ' Fundamenta Informaticae ' 18, 163-182 (1993).

@

A. Leitsch

(1993):
Resolution theorem proving.
AILA preprint 15,
Associazione Italiana di Logica e sue Applicazioni (1993).

@

A. Leitsch, G. Gottlob

(1990): 'Deciding clause implication problems by ordered semantic resolution ':
In: F. Gardin and G. Mauri (eds.): 'Computational Intelligence ' II, 19-26,
North-Holland (1990).

@

H.R. Lewis

(1979):
Unsolvable classes of quantificational formulas.
Addison Wesley (1979).

@

D.W. Loveland

(1970):
A linear format for resolution.
Proc. IRIA Symposium on Automatic Demonstration,
In: ' Lecture Notes in Mathematics ' 125, 147-162,
Springer (1970).

@

D.W. Loveland

(1978):
Automated theorem proving - a logical basis.
North Holland (1978).

@

J.W. Lloyd

(1987):
Foundations of logic programming.
Springer (2nd ed. 1987). L. Löwenheim (1915):
Über Möglichkeiten im Relativkalkül.
In: ' Math. Ann. ' 68, 169-207 (1915).

@

S.J. Lee, D. Plaisted

(1992):
Eliminating duplication with the hyperlinking strategy.
In: ' Journal of Automated Reasoning ' 9 (1), 25-42 (1992).

@

D. Luckham

(1970):
Refinements in resolution theory.
Proc. IRIA Symposium on Automatic Demonstration,
In: ' Lecture Notes in Mathematics ' 125, 163-190,
Springer (1970).

@

R. Manthey, F. Bry

(1988):
Satchmo: a theorem prover implemented in Prolog.
CADE 9, 'Lecture Notes in Computer Science ' 310, 415-434,
Springer (1988).

@

S.Y. Maslov

(1964):
An inverse method of establishing deducibilities in the classical predicate calculus.
In: ' Dokl. Akad. Nauk SSSR ' 159, 1420-1424 (1964).

@

S.Y. Maslov

(1968):
The inverse method of establishing deducibility for logical calculi.
Proc. Steklov 'Inst. Math. ' 98, 25-96 (1968).

@

R. Matzinger

(1993):
On lock resolution and decision methods for clause classes.
Master's thesis,
Dept. of Computer Science, Technische Universität Wien (1993).

@

W. McCune

(1990):
Otter 2.0 users guide.
Argonne National Laboratory, Argonne (1990).

@

G.E. Mints

(1990, 1993):
Gentzen-type systems and resolution rules. Part II: Predicate Logic.
In: ' Logic Colloquium ' 1990, 'Lecture Notes in Logic ' 2, 163-190,
Springer (1993).

@

A. Martelli, U. Montanari

(1982):
An efficient unification algorithm.
In: ' ACM Transactions on Programming Languages and Systems ' 4 (2), 258-282 (1982).

@

J. Marcinkowski, L. Pacholski

(1992):
Undecidability of the Horn clause implication problem.
In: ' Rapport de Recherche 1992-5 ',
Groupe de recherche algorithmique et logique, University of Caen, France (1992).

@

N.V. Murray, E. Rosenthal

(1985):
Path resolution and semantic graphs.
Proc. of the EUROCAL '85,
In: ' Lecture Notes in Computer Science ' 204, 50-63,
Springer (1985).

@

H. de Nivelle

(1996):
Resolution games and non-liftable orderings.
In: ' Collegium Logicum ', 'Annals of the Kurt Gödel Society ' 2, 1-20 (1996).

@

J. Pearl

(1984):
Heuristics: Intelligent search strategies for computer problem solving.
Addison-Wesley (1984).

@

J. Pellizzari

(1994):
Methods of function introduction.
Master's thesis,
Dept. of Computer Science, Technische Universität Wien (1994).

@

D. Prawitz

(1969):
Advances and problems in mechanical proof procedures.
In: ' Machine Intelligence ' 4, 59-71,
Elsevier (1969).

@

D. Prawitz

(1971):
Ideas and results in proof theory.
In: J.E. Fenstad (ed.): 'Proc. of the 2nd Scandinavian Logic Symposium ', 235 -308.
North-Holland (1971).

@

M.S. Paterson, M.N. Wegmam

(1978):
Linear unification.
In: ' Journal of Computer and System Sciences ' 16 (2), 158-167 (1978).

@

J.A. Robinson

(1965):
A machine oriented logic based on the resolution principle.
In: ' Journal of the ACM ' 12 (1), 23-41 (1965).

@

J.A. Robinson

(1965):
Automatic deduction with hyperresolution.
In: ' Intern. Journal of Comp. Math. ' 1, 227-234 (1965).

@

J.A. Robinson

(1979):
Logic: form and function.
North-Holland (1979).

@

V. Rudenko

(1992):
Decision of a Horn clause implication class with ≤ 2 variables in the head.
In: ' Yearbook of the Kurt Gödel Society ' 1992, 31-91.

@

T. Skolem

(1920):
Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen.
In: ' J.E. Fenstad (ed.): 'Selected works in logic by Th. Skolem ', 'Universitetsforlaget Oslo-Bergen-Troms ', 103-136 (1970). '

@

J.R. Slagle

(1967):
Automatic theorem proving with renamable and semantic resolution.
In: ' Journal of the ACM ' 14 (4), 687-697 (1967).

@

J. Slaney

(1992):
Finder (finite domain enumerator): notes and guide.
Technical Report TR-ARP-1/92,
Australian National University Automated Reasoning Project, Canberra (1992).

@

J. Slaney

(1993):
Scott: A model-guided theorem prover.
Proc. of the IJCAI '93, vol. 1, 109-114,
Morgan Kaufmann (1993).

@

E. Specker, V. Strassen

(1976):
Komplexität von Entscheidungsproblemen.
In: ' Lecture Notes in Computer Science ' 43,
Springer (1976).

@

M. Schmidt-Schauss

(1988):
Implication of clauses is undecidable.
In: ' Theoretical Computer Science ' 59, 287-296 (1988)

@

R. Statman

(1979):
Lower bounds on Herbrand's theorem.
In: ' Proc. AMS ' 75, 104-107 (1979).

@

S. Stenlund

(1971):
Combinators, &lambda;-terms and proof theory.
Reidel (1971).

@

R.B. Stillman

(1973):
The concept of weak substitution in theorem proving.
In: ' Journal of the ACM ' 20 (4), 648-667 (1973).

@

G. Takeuti

(1975):
Proof theory.
North-Holland (1975).

@

T. Tammet

(1991):
Using resolution for deciding solvable classes and building finite models.
In: ' Lecture Notes in Computer Science ' 502, 33-64,
Springer (1991).

@

G.S. Tseitin

(1983):
On the complexity of derivation in propositional calculus.
In: J. Siekmann, G. Wrightson (eds.): 'Automation of reasoning ', 466-483.
Springer (1983).

@

A. Turing

(1936-37):
On computable numbers with an application to the Entscheidungsproblem.
In: ' Proc. of the London Math. Soc. ' Ser. 2 42, 230-265 (1936/37).

@

L. Wos, G.A. Robinson, D.F. Carson

(1965):
Efficiency and completeness of the set of support strategy in theorem proving.
In: ' Journal of the ACM ' 12 (4), 536-541 (1965).

@

N.K. Zamov

(1972):
On a bound for the complexity of terms in the resolution method.
In: ' Proc. of the Steklov Math. Inst. ' 128, 5-13 (1972).