scientific article; zbMATH DE number 549974
From MaRDI portal
zbMath0797.03009MaRDI QIDQ4287493
Nicolas Zabel, Ricardo Caferra
Publication date: 17 October 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
unificationdecision proceduremodel constructiondisunificationequational problemsextension of resolutionsimultaneous search for a refutation and Herbrand models
Related Items
On the complexity of equational problems in CNF, Simplifying and generalizing formulae in tableaux. Pruning the search space and building models, A method for simultaneous search for refutations and models by equational constraint solving, MACE4 and SEM: A Comparison of Finite Model Generators, Combining enumeration and deductive techniques in order to increase the class of constructible infinite models, On deciding subsumption problems, A method for building models automatically. Experiments with an extension of OTTER, 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
