Simple tools for teaching logic are presented.
These softwares are made available to all, with the support of the
VERIMAG laboratory.
- Propositional logic
- First order logic
- Proof in first order logic by resolution
Given a list of clauses, as well as limits on the time of proof and the size of the clauses,
the software tries to build a proof of the empty clause within the imposed limits.
The prover is complete : if the set of clauses is unsatisfiable and if there is no limit on time
of proof and size of clauses, it will deduce the empty clause.
- Strategy "prover9" in first order logic
We have two lists of clauses, one is the support list and the other is the usable list.
From these two lists, the software tries to build a proof of the empty clause within the imposed limits.
The prover is complete, that means, if the usable list is satisfiable and if the set of all clauses is
unsatisfiable, and if there is no limit of time of proof and size of the clauses,
it will deduce the empty clause.
- Proof in first order logic by the Model
Elimination method
Given a list of clauses, as well as limits on the time and length of proof, the software tries
to build a proof by this method.
The prover is complete : if the set of clauses is unsatisfiable and if there is no limit on time
and length of proof, it will deduce the empty clause.
Last change : 02-Dec-2019