Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Cover of the book
Tytuł książki

Theorem-proving systems

Seria
Rozprawy Matematyczne tom/nr w serii: 103 wydano: 1973
Zawartość
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
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
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

JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.