Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria

DOI10.1006/jsco.1999.0361zbMath0969.03019OpenAlexW2076932470MaRDI QIDQ5927983

Reinhard Pichler

Publication date: 19 March 2001

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/jsco.1999.0361

zbMATH Keywords

atomic representationdecision problemsHerbrand modelstruth evaluation

Mathematics Subject Classification ID

Related Items (1)

On the complexity of equational problems in CNF

Uses Software

• LogiMOO

Cites Work

• Explicit representation of terms defined by counter examples
• Equational problems and disunification
• Proving termination with multiset orderings
• An Efficient Unification Algorithm
• Hyperresolution and automated model building
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Speeding up algorithms on atomic representations of Herbrand models via new redundancy criteria