scientific article; zbMATH DE number 1348470
From MaRDI portal
Publication:4264723
zbMath0925.03052MaRDI QIDQ4264723
No author found.
Publication date: 10 October 1999
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (24)
Automatic proofs and counterexamples for some ortholattice identities ⋮ Improving transformation systems for general E-unification ⋮ On narrowing, refutation proofs and constraints ⋮ AC-complete unification and its application to theorem proving ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Lazy narrowing: Strong completeness and eager variable elimination (extended abstract) ⋮ Superposition for higher-order logic ⋮ SMELS: Satisfiability Modulo Equality with Lazy Superposition ⋮ Unnamed Item ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Redundancy criteria for constrained completion ⋮ A total AC-compatible ordering based on RPO ⋮ R n - and G n -logics ⋮ On the complexity of recursive path orderings ⋮ Harald Ganzinger’s Legacy: Contributions to Logics and Programming ⋮ The Blossom of Finite Semantic Trees ⋮ Redundancy criteria for constrained completion ⋮ Superposition with Delayed Unification ⋮ Associative-commutative deduction with constraints ⋮ AC-superposition with constraints: No AC-unifiers needed ⋮ Local simplification ⋮ The Clause-Diffusion theorem prover Peers-mcd (system description) ⋮ What you always wanted to know about rigid E-unification ⋮ SMELS: satisfiability modulo equality with lazy superposition
Uses Software
This page was built for publication:
