scientific article; zbMATH DE number 1552532
From MaRDI portal
Publication:4524792
zbMATH Open0973.68215MaRDI QIDQ4524792FDOQ4524792
Authors: Leo Bachmair, Harald Ganzinger 
Publication date: 3 July 2001
Title of this publication is not available (Why is that?)
Recommendations
Cited In (41)
- Blocking and other enhancements for bottom-up model generation methods
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Positive deduction modulo regular theories
- A superposition oriented theorem prover
- Inferring Congruence Equations Using SAT
- Equality reasoning in sequent-based calculi
- Horn equational theories and paramodulation
- \(I\)-terms in ordered resolution and superposition calculi: retrieving lost completeness
- Equational theorem proving modulo
- Harald Ganzinger's legacy: contributions to logics and programming
- Title not available (Why is that?)
- Paramodulation-based theorem proving
- Superposition and Model Evolution Combined
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Model-theoretic methods in combined constraint satisfiability
- The anatomy of Equinox -- an extensible automated reasoning tool for first-order logic and beyond (talk abstract)
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- A combined superposition and model evolution calculus
- A comprehensive framework for saturation theorem proving
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- Selecting the selection
- A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
- The disconnection tableau calculus
- Resolution with order and selection for hybrid logics
- Superposition with equivalence reasoning and delayed clause normal form transformation.
- The equational part of proofs by structural induction
- Automated reasoning building blocks
- Model evolution with equality -- revised and implemented
- A comprehensive framework for saturation theorem proving
- Computing All Implied Equalities via SMT-Based Partition Refinement
- Paramodulation with non-monotonic orderings and simplification
- Superposition with equivalence reasoning and delayed clause normal form transformation
- The model evolution calculus as a first-order DPLL method
- Quantifier Elimination and Provers Integration
- First-order resolution methods for modal logics
- Combining superposition, sorts and splitting
- Computer Science Logic
- Connection calculus theorem proving with multiple built-in theories
- Equational Theorem Proving for Clauses over Strings
- Title not available (Why is that?)
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4524792)
