SATCHMO: A theorem prover implemented in Prolog

Lecture notes in computer sciencePublished 23 November 2005Open access

Rainer Manthey, François Bry

Citations283

TL;DR

The paper provides a thorough report on experiences with SATCHMO, a theorem prover consisting of just a few short and simple Prolog programs that is refutation-complete if used in a level-saturation manner.

Abstract

Satchmo is a theorem prover consisting of just a few short and simple Prolog programs. Prolog may be used for representing problem clauses as well. SATCHMO is based on a model-generation paradigm. It is refutation-complete if used in a level-saturation manner. The paper provides a thorough report on experiences with SATCHMO. A considerable amount of problems could be solved with surprising efficiency.

Keywords

Computer Science

Medical Entomology and ZoologyFirst-Order Logic

1,124 Citations1968Raymond M. Smullyan

First-Order Logic

677 Citations1968Raymond M. Smullyan

Acta InformaticaLogic for improving integrity checking in relational data bases?

307 Citations1982Jean‐Marie Nicolas

The purpose of this paper is to present a simplification method yielding such simplified forms for integrity constraints which depend on the nature of the updating operation which is the cause of the state change.

Lecture notes in computer scienceA uniform approach to constraint satisfaction and constraint satisfiability in deductive databases

135 Citations1988François Bry, Hendrik Decker +1 more

A satisfiability checking method is presented that employs integrity maintenance techniques and checks constraint satisfiability, i.e., whether a database exists in which all constraints are simultaneously satisfied.

New Generation ComputingA Prolog technology theorem prover

99 Citations1984Mark E. Stickel

An extension of Prolog, based on the model elimination theorem-proving procedure, would permit production of a logically complete Prolog technology theorem prover capable of performing inference operations at a rate approaching that of prolog itself.

Lecture notes in computer sciencePaths to high-performance automated theorem proving

14 Citations1986Ralph Butler, Ewing Lusk +2 more

Four components of a strategy for the implementation of high-performance automated theorem proving systems are described and how they can be integrated into a coherent system with significantly higher performance than traditional systems are shown.

Informatik-FachberichteA Hyperresolution-based Proof Procedure and Its Implementation in Prolog

12 Citations1987Rainer Manthey, François Bry

The procedure described in this paper is the basis of a program called SATCHMO (SATisfiability CHecking by MOdel generation) that has been implemented at ECRC as part of a prototype schema design system for logic databases.

View PDF