If you consult this site for the first time, read the Introduction.

This site offers programs computing the following functions:

decide[FOL-expression] decides whether FOL-expression is False or sat.

See Introduction for further information.

model[FOLexpression,upperbound] returns a finite model for a formula of pure first-order logic if there is such a model within a domain of natural numbers up to upperbound. If there is only a finite or infinite model with a cardinality of a domain that goes beyond upperbound a series of transcendent models is returned that converges to such a model unless it is predictable by the syntax of the formula that there is a finite model. In this case `Try again with an increased upperbound' is returned.

pureoptimizer[FOLexpression] converts FOLexpressions to optimized DNFFOLs by pure logical equivalence transformation. This function is an equivalent to the Quine-McCluskey algorithm for pure FOL.

This is a test version for a prover and disprover based on resolution and skolemization.

© Timm Lampert / 2018-02-09