Skolem Machines

• Autorzy: Fisher J. , Bezem M.
• Języki publikacji: EN

Abstrakty

EN

The Skolem machine is a Turing-complete machine model where the instructions are first-order formulas of a specific form. We introduce Skolem machines and prove their logical correctness and completeness. Skolem machines compute queries for the Geolog language, a rich fragment of first-order logic. The concepts of Geolog trees and complete Geolog trees are defined, and these tree concepts are used to show logical correctness and completeness of Skolem machine computations. The universality of Skolem machine computations is demonstrated. Lastly, the paper outlines implementation design issues using an abstract machine model approach.

Słowa kluczowe

EN

finitary geometric logic; Skolem machines; Geolog language; Geolog trees; correctness; completeness; universality

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 91, nr 1
• Strony: 79--103
• Opis fizyczny: bibliogr. 19 poz., wykr.

Twórcy

autor

Fisher J.

autor

Bezem M.

• Department of Computer Science, California State Polytechnic University Pomona, California, USA,

Bibliografia

• [1] H. Ait-Kaci, Warrens's Abstract Machine, A Tutorial Reconstruction, School of Computing Science, February 18, 1999.
• [2] M. Bezem and T. Coquand. Newman's Lemma - a Case Study in Proof Automation and Geometric Logic. In Y. Gurevich, editor, The Logic in Computer Science Column, Bulletin of the European Association for Theoretical Computer Science 79:86-100, February 2003. Also in G. Paun, G. Rozenberg and A. Salomaa, editors, Current trends in Theoretical Computer Science, Volume 2, pp. 267-282, World Scientific, Singapore, 2004.
• [3] M.A. Bezem and T. Coquand, Automating Coherent Logic. In G. Sutcliffe and A. Voronkov, editors, Proceedings LPAR-12, LNCS 3835, pages 246-260, Springer-Verlag, Berlin, 2005.
• [4] Marc Bezem. On the Undecidability of Coherent Logic. In Aart Middeldorp e.a., editors, Processes, Terms and Cycles: Steps on the Road to Infinity, LNCS 3838, pages 6-13, Springer-Verlag, Berlin, 2005.
• [5] A. Blass, Topoi and computation. Bulletin of the EATCS 36:57-65, October 1998.
• [6] Geolog website: http://www.csupomona.edu/ jrfisher/www/geolog
• [7] John Fisher and Marc Bezem, Skolem Machines and Geometric Logic. In C.B. Jones, Z. Liu and J. Woodcock, Proc. ICTAC 2007 The 4th International Colloquium on Theoretical Aspects of Computing, Macao SAR, China, September 26-28, 2007. Springer LNCS vol. 4711, pp. 201-215.
• [8] John Fisher and Marc Bezem, Query Completeness of Skolem Machine Computations. In J. Durand-Losé and M. Margenstern, editors, Proc. Machines, Computations and Universality '07, Universite d'Orleans - LIFO, Orleans, France September 10-14, 2007. Springer LNCS vol. 4664, pp. 182-192.
• [9] Jacques Herbrand, Logical Writings, edited by Warren D. Goldfarb, D. Reidel Publishing Company, Springer edition, 2006.
• [10] P. Johnstone, Sketches of an Elephant: a topos theory compendium, Volume 2, Oxford Logic Guides 44, OUP, 2002.
• [11] Dénes Kőnig, Theorie der endlichen und unendlichen Graphen, Akademische Verlagsgesellschaft, Leipzig, 1936. Translated from German by Richard McCoart, Theory of finite and infinite graphs, Birkhauser, 1990.
• [12] J.W. Lloyd, Foundations of Logic Programming, Springer-Verlag, Berlin, revised edition 1987.
• [13] Marvin L. Minsky, Recursive unsolvability of Post's problem of 'tag' and other topics in theory of Turing machines, Annals of Mathematics 74(3):437-455, 1961.
• [14] Nordic Journal of philosophical Logic 1(2) December 1996. Special issue devoted to the influence on logic of Thoralf Skolem.
• [15] R. Manthey and F. Bry, SATCHMO: A Theorem Prover Implemented in Prolog. In: E. Lusk and R. Overbeek, editors, Proceedings CADE-9, LNCS 310, pages 415-434, Springer-Verlag, Berlin, 1988.
• [16] H. de Nivelle and J. Meng, Geometric Resolution: A Proof Procedure Based on Finite Model Search. In: U. Furbach and N. Shankar, editors, Automated Reasoning, Proceedings IJCAR 2006, LNCS 4130, pages 303-317, Springer-Verlag, Berlin, 2006.
• [17] Thoralf Skolem, Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit und Beweisbarkeit mathematischen Sätze nebst einem Theoreme über dichte Mengen, Skrifter I 4:1-36, Det Norske Videnskaps-Akademi, 1920. Also in Jens Erik Fenstad, editor, Selected Works in Logic by Th. Skolem, pp. 103-136, Universitetsforlaget, Oslo, 1970.
• [18] D.H.D. Warren, Implementation of Prolog. Lecture notes of Tutorial No. 3, 5th International Conference and Symposium on Logic Programming, Seattle, WA, August 1988.
• [19] J. Wielemaker, SWI-Prolog Reference Manual. Link available at: www.swi-prolog.org