Efficient Algorithms for Bounded Rigid E-unification

DOI10.1007/978-3-319-24312-2_6zbMath1471.68300OpenAlexW2195777310MaRDI QIDQ3455762

Peter Backeman, Philipp Rümmer

Publication date: 11 December 2015

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

Full work available at URL: https://doi.org/10.1007/978-3-319-24312-2_6

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Free Variables and Theories: Revisiting Rigid E-unification ⋮ Congruence Closure with Free Variables ⋮ Fault-Tolerant Aggregate Signatures

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• What you always wanted to know about rigid \(E\)-unification
• Abstract congruence closure
• Theorem Proving with Bounded Rigid E-Unification
• Fast Decision Procedures Based on Congruence Closure
• Theorem proving using equational matings and rigid E -unification
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic