Automated Deduction – CADE-20

DOI10.1007/11532231zbMath1135.03325OpenAlexW2485416161MaRDI QIDQ5394627

Peter Baumgartner, Cesare Tinelli

Publication date: 1 November 2006

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11532231

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

The model evolution calculus as a first-order DPLL method ⋮ The disconnection tableau calculus ⋮ Superposition-based equality handling for analytic tableaux ⋮ Model evolution with equality -- revised and implemented ⋮ Superposition as a decision procedure for timed automata ⋮ A combined superposition and model evolution calculus ⋮ Planning with Effectively Propositional Logic ⋮ The Relative Power of Semantics and Unification ⋮ A sound and complete model-generation procedure for consistent and confidentiality-preserving databases ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Superposition and Model Evolution Combined ⋮ Model Evolution with Equality Modulo Built-in Theories ⋮ First order Stålmarck. Universal lemmas through branch merges ⋮ SCL(EQ): SCL for first-order logic with equality