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
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, 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
