The New Logic Project


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.



Powered by webMathematica

Datenschutzerklaerung

© Timm Lampert / 2018-02-09