LITERATUURFormele 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):@ 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, '@ 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). |
||
|
||