Free Variables and Theories: Revisiting Rigid E-unification

DOI10.1007/978-3-319-24246-0_1zbMath1471.68301OpenAlexW2259620693MaRDI QIDQ2964448

Philipp Rümmer, Peter Backeman

Publication date: 27 February 2017

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24246-0_1

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The undecidability of simultaneous rigid E-unification
• What you always wanted to know about rigid \(E\)-unification
• Theorem Proving with Bounded Rigid E-Unification
• Efficient Algorithms for Bounded Rigid E-unification
• Presburger arithmetic with unary predicates is Π₁¹ complete
• Theorem proving using equational matings and rigid E -unification
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic

This page was built for publication: Free Variables and Theories: Revisiting Rigid E-unification