Finfimo home page

Finfimo is a depth-first implementation of the EP Tableaux Method, using a concise Prolog program in the style of Satchmo. Depth-first search does not guarantee completeness for Finite Satisfiability, but breadth-first search does. The application SIC uses a breadth-first implementation of the EP Tableaux Method.

Information about Finfimo

The underlying method is described in: A Deduction Method Complete for Refutation and Finite satisfiability.
An application of Finfimo is described in: SIC: Satisfiability Checking for Integrity Constraints.

The Program Finfimo

Finfimo.
Tools.

Sunna.Torge@informatik.uni-muenchen.de