Publication:4287493
From MaRDI portal
zbMath0797.03009MaRDI QIDQ4287493
Ricardo Caferra, Nicolas Zabel
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
MACE4 and SEM: A Comparison of Finite Model Generators, 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