Inspired by the wonderful design and implementation of the Prolog language afforded by the Warren Abstract Machine (WAM), this paper describes an extended logical language which can compute larger realms of first-order logic, based upon theories for finitary geometric logic. The paper describes a Geolog language for expressing first-order geometric logic in tidy closed form, a mathematical Skolem Machine that computes the language, and an implementation prototype that intimately mimics the abstract machine, and which also reformulates expensive bottom-up inference into efficient top-down inference. There are promising mathematical theorem proving applications for geometric logic systems, collected on the website [5]. The emphasis of this paper is theory, abstract machine design and direct implementation of the abstract machine. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Fisher, J., & Bezem, M. (2007). Skolem machines and geometric logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4711 LNCS, pp. 201–215). Springer Verlag. https://doi.org/10.1007/978-3-540-75292-9_14
Mendeley helps you to discover research relevant for your work.