Literatuur_formele_logica

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. In: 'Proc. CSL', '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. In: ' 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 . In: '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, λ-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).


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. In: 'Proc. CSL', '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. In: ' 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 . In: '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, λ-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).