Theorem Proving with Bounded Rigid E-Unification

DOI10.1007/978-3-319-21401-6_39zbMath1431.03022OpenAlexW1419398250MaRDI QIDQ3454123

Philipp Rümmer, Peter Backeman

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_39

Mathematics Subject Classification ID

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

Related Items (4)

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

Cites Work

• What you always wanted to know about rigid \(E\)-unification
• Abstract congruence closure
• E-Matching with Free Variables
• Hyper Tableaux with Equality
• Theorem proving using equational matings and rigid E -unification
• Automated Reasoning with Analytic Tableaux and Related Methods
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Theorem Proving with Bounded Rigid E-Unification