Free variables and theories: revisiting rigid E-unification

DOI10.1007/978-3-319-24246-0_1zbMATH Open1471.68301OpenAlexW2259620693MaRDI QIDQ2964448FDOQ2964448

Authors: Peter Backeman, Philipp Rümmer 

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

Recommendations

• Theorem proving with bounded rigid \(E\)-unification
• Efficient algorithms for bounded rigid \(E\)-unification
• scientific article; zbMATH DE number 1552529
• What you always wanted to know about rigid \(E\)-unification
• Special cases and substitutes for rigid \(E\)-unification

Mathematics Subject Classification ID

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

Cites Work

• Presburger arithmetic with unary predicates is Π₁¹ complete
• Title not available (Why is that?)
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• What you always wanted to know about rigid \(E\)-unification
• Theorem Proving with Bounded Rigid E-Unification
• Theorem proving using equational matings and rigid E -unification
• The undecidability of simultaneous rigid E-unification
• Equality reasoning in sequent-based calculi
• Title not available (Why is that?)
• Title not available (Why is that?)
• Efficient Algorithms for Bounded Rigid E-unification

This page was built for publication: Free variables and theories: revisiting rigid \(E\)-unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2964448)