• Raphael Cauderlier's avatar
    Pairs of quantified clauses · 481f3b33
    Raphael Cauderlier authored
    This structure is intended to be used for resolution and
    paramodulation tactics. Having both clauses under the same quantifiers
    allows to perform shallow unification.
    481f3b33
Name
Last commit
Last update
example Loading commit data...
fol Loading commit data...
meta Loading commit data...
.gitignore Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
README.org Loading commit data...
configure Loading commit data...
manual.org Loading commit data...
opam Loading commit data...
version.txt Loading commit data...