The following pages link to (Q4264723):
Displaying 23 items.
- Automatic proofs and counterexamples for some ortholattice identities (Q293265) (← links)
- Redundancy criteria for constrained completion (Q673620) (← links)
- A total AC-compatible ordering based on RPO (Q673623) (← links)
- On the complexity of recursive path orderings (Q685537) (← links)
- Conditional congruence closure over uninterpreted and interpreted symbols (Q1730315) (← links)
- Linear and unit-resulting refutations for Horn theories (Q1923821) (← links)
- SMELS: satisfiability modulo equality with lazy superposition (Q2351265) (← links)
- SMELS: Satisfiability Modulo Equality with Lazy Superposition (Q3540073) (← links)
- (Q4222859) (← links)
- R n - and G n -logics (Q4645806) (← links)
- Harald Ganzinger’s Legacy: Contributions to Logics and Programming (Q4916069) (← links)
- The Blossom of Finite Semantic Trees (Q4916075) (← links)
- Redundancy criteria for constrained completion (Q5055781) (← links)
- Improving transformation systems for general E-unification (Q5055788) (← links)
- On narrowing, refutation proofs and constraints (Q5055818) (← links)
- AC-complete unification and its application to theorem proving (Q5055849) (← links)
- Local simplification (Q5096297) (← links)
- Lazy narrowing: Strong completeness and eager variable elimination (extended abstract) (Q5096745) (← links)
- Associative-commutative deduction with constraints (Q5210795) (← links)
- AC-superposition with constraints: No AC-unifiers needed (Q5210796) (← links)
- The Clause-Diffusion theorem prover Peers-mcd (system description) (Q5234687) (← links)
- What you always wanted to know about rigid E-unification (Q5235253) (← links)
- Superposition for higher-order logic (Q6156638) (← links)
