Publication:4287493
From MaRDI portal
zbMath0797.03009MaRDI QIDQ4287493
Nicolas Zabel, Ricardo Caferra
Publication date: 17 October 1994
unification; decision procedure; model construction; disunification; equational problems; extension of resolution; simultaneous search for a refutation and Herbrand models
03B35: Mechanization of proofs and logical operations
Related Items
Simplifying and generalizing formulae in tableaux. Pruning the search space and building models, MACE4 and SEM: A Comparison of Finite Model Generators, A method for building models automatically. Experiments with an extension of OTTER, Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, A method for simultaneous search for refutations and models by equational constraint solving, On the complexity of equational problems in CNF, On deciding subsumption problems, Explicit versus implicit representations of subsets of the Herbrand universe., Efficient model generation through compilation., Working with ARMs: Complexity results on atomic representations of Herbrand models