Theorem-proving systems

Orłowska, Ewa

Książka - szczegóły

Tytuł książki

Theorem-proving systems

Autorzy

Ewa Orłowska

Seria

Rozprawy Matematyczne tom/nr w serii: 103 wydano: 1973

Zawartość

Pełne teksty:

Pobierz

Warianty tytułu

Abstrakty

EN

CONTENTS
Introduction.................................................................................................................... 6
Chapter I. Theorem-proving system
§ 1. Theory...................................................................................................................... 7
§ 2. Fundamental theory $T_ƒ$ ................................................................................ 8
§ 3. Theorem-proving system.................................................................................... 16
Chapter II. Theorem-proving process
§ 1. Diagram of a formula........................................................................................... 20
§ 2. The set T of partial diagrams.............................................................................. 20
§ 3. Properties of the set T of partial diagram......................................................... 22
§ 4. Theorem-proving process........................................................................ 27
Chapter III. Properties of theorem-proving systems
§ 1. Existence and uniqueness of an unextendable process.............................. 32
§ 2. Properties of the set of theorem-proving processes..................................... 33
§ 3. C- systems............................................................................................................. 36
§ 4. Equivalence of theorem-proving systems........................................................ 38
§ 5. Theorem-proving algorithms.............................................................................. 43
References.................................................................................................................... 48

Słowa kluczowe

Tematy

Wydawca

Instytut Matematyczny Polskiej Akademii Nauk

Miejsce publikacji

Warszawa

Copyright

Seria

Rozprawy Matematyczne tom/nr w serii: 103

Liczba stron

51

Liczba rozdzia³ów

Opis fizyczny

Dissertationes Mathematicae, Tom CIII

Daty

wydano

1973

Twórcy

autor

Ewa Orłowska

Bibliografia

[1] W. Z. Ackermann, Solvable oases of the decision problem, Amsterdam 1964.
[2] P. B. Andrews, Resolution with merging, J. ACM 15 (3) (1968).
[3] J. Allen and E). Luckham, An interactive theorem proving program, Machine Intelligence (1970), pp. 321-336.
[4] J. H. Bennett, CRT-Aided Semi-Automated Mathematics, Report AFCRL-67-0167, Applied Logic Corporation, Princeton 1967.
[5] E. W. Beth, Semantic entailment and formal derivability, Med. der Kon. Nederl. Akad. van Wetensch. 18 (13) (1955).
[6] E. W. Beth, On machines which prove theorems, Simon Stevin (Wissen Naturkundig Tijdschrift) 32 (1958), pp. 49-60.
[7] Т. C. Brown, Resolution with covering strategies and equality theory, California 1968.
[8] C. L. Chang, Renamable paramodulation for automatic theorem-proving with equality, Bethseda, Maryland 1969.
[9] M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM 7 (1960), pp. 201-215.
[10] M. Davis, Eliminating the irrelevant from mechanical proofs, Proc. Symp. Appl. Math. 15 (1963), pp. 15-30.
[11] M. Davis, G. Logemann and D, Loveland, A machine program for theorem-proving. C. ACM 5 (1962), pp. 394-397.
[12] J. L. Darlington, Theorem proving and information retrieval, Machine Inteligence 4 (1969), pp. 173-181.
[13] J. L. Darlington, Automatic theorem-proving with equality substitution and mathematical induction, Machine Intelligence (1968), pp. 113-127,
[14] J. Doran and D. Michie, Experiments with the graph traverser program, Proc. Royal Society (A) 294 (1966), pp. 235-259.
[15] B. Dreben, Systematic treatment of the decision problem, Summer Institute for Symbolic Logic, Cornell Univ. (1957).
[16] B. Dunham and J. H. North, Theorem testing by computer, Sympos. Math, Theory Automata, Brooklyn Politechnic Institute, Brooklyn 1962.
[17] B. Dunham, R. Fridshall and G. L. Sward, A nonheuristic program for proving elementary logical theorems, Proc. First Intern. Conference on Information Processing, Paris 1959, p. 282.
[18] A. Ehrenfeucht and E. Orłowska, Mechanical proof procedure for propsitinal calculus, Bulletin de l'Academie Polonaise des Sciences, Série des sciences math. astr. et phys, 15 (1) (1967), pp. 25-30.
[19] J. Fridman, A semi-decision procedure for the functional calculus, J. ACM 10 (1963), pp. 1-24.
[20] J. Fridman, A computer program for a solvable case of the decision problem, J. ACM 10 (1963), pp. 348-356.
[21] J. Fridman, Extensions of two solvable oases of the decision problem, J. Symb. Logic 22 (1957).
[22] G. Gentzen, Untersuchungen über des logische Schliessen, Mathematische Zeitschrift 39 (1934).
[23] P. C. Gilmore, A proof method for quantification theory, IBM J. Res. Develop. 4 (1960), pp. 28-35.
[24] P. C. Gilmore, A program for the production of proofs for theorems derivable within the first order predicate calculus from axioms, Proc. of the First Internat. Conference on Information Processing, Paris 1959.
[25] W. E. Gould, A matching procedure for w-order logic, Science Report 4 (1966), pp. 66-781.
[26] J. R. Guard, P. C. Oglesby, J. H. Bennet and L. G. Settle, Semi automated mathematics, J. ACM 16 (1969), pp. 49-62.
[27] T. P. Hart, A useful algebraic property of Robinson's unification algorithm, Artificial Intelligence Project Memo 91, Project MAC, MIT, Cambridge, Massachusetts (1965).
[28] P. J. Hayes and R. A. Kowalski, Semantic tress in automatic theorem proving, Machine Intelligence 4 (1969), pp. 84-101.
[29] J. Herbrand, Recherches sur la théorie de la démonstration, Travaux de la Société des Sciences at des Lettres de Varsovie, Classe III sciences mathématiques et physiques 33 (1930).
[30] J. Herbrand, Sur la problème fondamentale de la logique mathématique, Compt. rend. Soc. Sci. Lettres Varsovie, Classe III, 24 (1931), pp. 12-56.
[31] S. Kanger, Probability in Logic, Stockholm 1957 (Stud, in phil.)
[32] S. Kanger, A simplified proof method for elementary logic, Computer programing and formal systems, Studies in Logic and the Pound of Math., Amsterdam 1963.
[33] V. G. Kirin, Ujęcia algebraiczne i gentzenowskie logik Posta, Uniwersytet Warszawski, Warszawa 1966.
[34] S. C. Kleene, Permutability of inferences in Gentzen's calculi LK and LJ. Memoirs Amer. Math. Soc. (10), pp. 1-26.
[35] R. A. Kowalski, Formal systems and non-numerical problem solving by computers, Fourth Systems Symposium, Case Western Reserve University, Cleveland, Ohio 1968.
[36] R. A. Kowalski, The case for using equality axioms in automatic demonstration, Proceedings IRIA, Symposium on Automatic Demonstration, Versailles, 1968.
[37] R. A. Kowalski, Search strategies for theorem proving, Machine Intelligence 5 (1970), pp. 181-201.
[38] D. W. Loveland, Mechanical Theorem Proving by Model Elimination, J. ACM 15 (1968), pp. 236-261.
[39] D. W. Loveland, A linear format for resolution, Proceedings IRIA Symposium on Automatic Demonstration, Versailles 1968.
[40] D. Luckham, Some Tree-Paring Strategies for Theorem-Proving, Machine Intelligence 3 (1968), pp. 95-112.
[41] D. Luckham, Refinement theorems in resolution theory, Proc. IRIA Symposium on Automatic Demonstration, Versailles 1968.
[42] B. Meltzer, Power amplification for theorem provers, Machine Intelligence 5 (1970), pp. 165-179.
[43] B. Meltzer, Theorem proving for computers: some results on resolution and renaming, Computer J. 8 (1966), pp. 341-343.
[44] B. Meltzer, The Use of Symbolic Logic in Proving Mathematical Theorems by Means of a Digital Computer, "Foundations of Mathematics", ed. Prof. Hahn 1968.
[45] B. Meltzer, Logic and the formalization of mathematics, Science Progress, Oxford, 55 (1967), pp. 583-595.
[46] B. Meltzer, Some notes on resolution strategies, Machine Intelligence 3 (1968), pp. 71-76.
[47] B. Meltzer, A new look at mathematics and its mechanization, Machine Intelligence 3 (1968), pp. 63-70.
[48] J. B. Morris, E-resolution: extension of resolution to include the equality relation, Proc. International Joint Conference on Artificial Intelligence, Washington D.C. (7-9 May, 1969), pp. 287-294.
[49] E. Orłowska, Mechanical proof procedure for the n-valued propositional calculus, Bull, de l'Academie Polonaise des Sciences. Série des siences math., astr. et phys. 15 (8) (1967), pp. 537-541.
[50] E. Orłowska, Mechanical theorem proving in a certain class of formulae of the predicate calculus, Studia Logica 25 (1969), pp. 17-27.
[51] D. Prawitz, H. Prawitz and N. Vogera, A mechanical proof procedure and its realization in an electronic computer, J. ACM 7 (1960), pp. 101-128.
[52] D. Prawitz, Advances and Problems in Mechanical Proof Procedures, Report University of Stockholm 1967.
[53] W. Y. O. Quine, A proof procedure for quantification theory, J. Symb. Log. 20 (1955), pp. 141-149.
[54] B. Raphael, Some results about proof by resolution, SIGART Newsletter 14 (February 1969), pp. 22-25.
[55] H. Rasiowa and R. Sikorski, The Mathematics of Metamathematics, Warszawa 1970.
[56] G. A. Robinson and L. Wos, Paramodulation and theorem-proving in first-order theories with equality, Machine Intelligence 4 (1969), pp. 135-150.
[57] G. A. Robinson and L. Wos, Completeness of paramodulation, Abstract. J. of Symbolic Logic 34 (1969), p. 160.
[58] G. A. Robinson and L. Wos, and D. P. Carson, Some theorem proving strategies and their implementation, AMD Tech. Memo 72, Argonne Nat. Laboratory 1964.
[59] G. A. Robinson, A machine oriented logic based on the resolution principle, J. ACM 12 (1965), pp. 23-41.
[60] G. A. Robinson, Theorem-proving on the computer, J. ACM 10 (1963), pp. 163-174.
[61] G. A. Robinson, Automatic deduction with hyper resolution, Int. J. Computer Math. 1 (1965), pp. 227-234.
[62] G. A. Robinson, The generalised resolution principle, Machine Intelligence 3 (1968), pp. 77 - 93.
[63] G. A. Robinson, New direction in mechanical theorem-proving, IFIP Congres 68, Amsterdam 1969.
[64] G. A. Robinson, A Review of automatic theorem-proving, Proc. Symposia in Applied Mathematics 19, Mathematical Aspects of Computer Science, American Mathematical Society, 1967.
[65] G. A. Robinson, Heuristic and complete processes in the mechanization of theorem-proving, System and Computer Science (1967), pp. 116-124.
[66] G. A. Robinson, Mechanizing higher-order logic, Machine Intelligence 4 (1969), pp. 151-170.
[67] G. A. Robinson, The present state of mechanical theorem proving, Proc. Fourth Systems Symposium 1968.
[68] J. R. Slagle, Automatic theorem proving with renamable and semantic resolution, J. ACM 14 (1967) pp. 687-697.
[69] J. R. Slagle, A proposed preference strategy using sufficiency — resolution for answering questions, Lawrence Radiation Laboratories Memo. UCRL-14361 (1965).
[70] J. R. Slagle, C. L. Chang and R. C. T. Lee, Completeness theorems for semantic resolution in consequence finding, Proc. Intern. Joint Conference on Artificial Intelligence, Washington D.C. (7-9 May, 1969), pp. 281-285.
[71] E. E. Sibert, A machine-oriented logo incorporating the equality relation, Ph. D. thesis, Rice University, Houston 1967.
[72] H. Wang, Formalization and automatic theorem proving, Proc. IFIP Congress 1 (1965).
[73] H. Wang, Towards mechanical mathematics, IBM J. Res. Develop. 4 (1960), pp. 2-22.
[74] H. Wang, Proving theorems by pathern recognition, Part I: C. ACM 3 (1960), pp. 220-234, Part II: Bell System Tech. J. 40 (1961), pp. 1-41.
[76] A. Wasilewska, A formalization of the modal propositional S4 calculus, Studia Logica 27 (1971).
[76] L. Wos, D. Carson and Gr. Robinson, The unit preference strategy in theorem proving, AFIPS Conf. Proc. 26 (1964), pp. 615-621.
[77] L. Wos, and Gr. A. Robinson, Maximal model theorem, Abstract, J. Symbolic Logic 34 (1969), pp. 159-160.
[78] L. Wos, and Gr. A. Robinson, and D. F. Carson, Efficiency and completeness of the set of support strategy in theorem proving, J. ASM 12 (1965), pp. 536-641.
[79] L. Wos, D. Carson, Gr. Robinson and I. Shalla, The concept of demodulation in theorem proving, J. ACM 14 (1967), pp. 698-709.

Języki publikacji

EN

Uwagi

Identyfikator YADDA

bwmeta1.element.zamlynska-ec871916-76dd-4c1e-b869-1ac1501692b0

Identyfikatory

Kolekcja

DML-PL

Zawartość książki

rozwiń roczniki

Książka - szczegóły

Theorem-proving systems

Autorzy

Seria

Zawartość

Warianty tytułu

Abstrakty

Słowa kluczowe

Tematy

Wydawca

Miejsce publikacji

Copyright

Seria

Liczba stron

Liczba rozdzia³ów

Opis fizyczny

Daty

Twórcy

Bibliografia

Języki publikacji

Uwagi

Identyfikator YADDA

Identyfikatory

Kolekcja