The ToyElim System

An experimental prototype system for the computational processing of logic formulas. It is centered around a single processing function which takes a formula of propositional logic extended with operators for projection and circumscription as input, and outputs an equivalent formula without these operators.

Tasks like elimination of Boolean quantifiers, computation of uniform interpolants, certain forms of abduction, SAT and QBF solving, and processing of formulas according to various semantics of logic programming can be expressed and integrated in this framework.

The objective of the system is to explore experimentally the approach to the computational processing of logics by operator elimination. The current implementation is basically a toy system which suffices for small applications. It however transparently passes identified SAT, QBF and variable elimination subproblems to efficient external solvers.

Caveats

This system is currently intended just as a vehicle for experiments of various kinds. The code is of miscellaneous quality and robustness.

Downloads