Affiliations: Department of Computer Science, California State
Polytechnic University, Pomona, California, USA. [email protected] | Department of Computer Science, University of Bergen,
Bergen, Norway. [email protected]
Note: [] Address for correspondence: Department of Computer Science,
California State Polytechnic University, Pomona, California, USA
Abstract: 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.
