scientific article; zbMATH DE number 1552532

zbMath0973.68215MaRDI QIDQ4524792

Leo Bachmair, Harald Ganzinger

Publication date: 3 July 2001

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

automated theorem provers

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

The model evolution calculus as a first-order DPLL method, Paramodulation with non-monotonic orderings and simplification, The disconnection tableau calculus, Equational Theorem Proving for Clauses over Strings, Resolution with order and selection for hybrid logics, Model evolution with equality -- revised and implemented, A combined superposition and model evolution calculus, Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \), Harald Ganzinger’s Legacy: Contributions to Logics and Programming, First-Order Resolution Methods for Modal Logics, Quantifier Elimination and Provers Integration, Connection calculus theorem proving with multiple built-in theories, Model-theoretic methods in combined constraint satisfiability, Superposition and Model Evolution Combined, Blocking and other enhancements for bottom-up model generation methods, Equational theorem proving modulo, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective