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.
© Timm Lampert / 2018-02-09