Pages that link to "Item:Q4302815"
From MaRDI portal
The following pages link to Theorem proving using equational matings and rigid <i>E</i> -unification (Q4302815):
Displaying 23 items.
- The undecidability of simultaneous rigid E-unification (Q671659) (← links)
- Superposition-based equality handling for analytic tableaux (Q877891) (← links)
- Rigid E-unification: NP-completeness and applications to equational matings (Q921913) (← links)
- Decidability and complexity of simultaneous rigid E-unification with one variable and related results (Q1575636) (← links)
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid \(E\)-unification (Q1810851) (← links)
- A uniform procedure for converting matrix proofs into sequent-style systems (Q1854382) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Variadic equational matching in associative and commutative theories (Q2029000) (← links)
- Free Variables and Theories: Revisiting Rigid E-unification (Q2964448) (← links)
- Theorem Proving with Bounded Rigid E-Unification (Q3454123) (← links)
- Efficient Algorithms for Bounded Rigid E-unification (Q3455762) (← links)
- Cyclic connections (Q4645228) (← links)
- Incremental theory reasoning methods for semantic tableaux (Q4645229) (← links)
- Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-unification (Q4647498) (← links)
- <scp>OutsideIn(X)</scp>Modular type inference with local assumptions (Q4918240) (← links)
- Efficient ground completion (Q5055736) (← links)
- A completion-based method for mixed universal and rigid E-unification (Q5210805) (← links)
- KoMeT (Q5210812) (← links)
- A practical integration of first-order reasoning and decision procedures (Q5234694) (← links)
- What you always wanted to know about rigid E-unification (Q5235253) (← links)
- Computer Science Logic (Q5311286) (← links)
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality (Q5747761) (← links)
- Simultaneous rigid E-unification is undecidable (Q6560168) (← links)