scientific article; zbMATH DE number 1552532
From MaRDI portal
Publication:4524792
Recommendations
Cited in
(41)- scientific article; zbMATH DE number 3986667 (Why is no real title available?)
- Blocking and other enhancements for bottom-up model generation methods
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- A superposition oriented theorem prover
- Positive deduction modulo regular theories
- 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
- scientific article; zbMATH DE number 1670742 (Why is no real title available?)
- Harald Ganzinger's legacy: contributions to logics and programming
- Paramodulation-based theorem proving
- Model-theoretic methods in combined constraint satisfiability
- Superposition and Model Evolution Combined
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- A combined superposition and model evolution calculus
- The anatomy of Equinox -- an extensible automated reasoning tool for first-order logic and beyond (talk abstract)
- Selecting the selection
- A comprehensive framework for saturation theorem proving
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- 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
- Paramodulation with non-monotonic orderings and simplification
- Computing All Implied Equalities via SMT-Based Partition Refinement
- A comprehensive framework for saturation theorem proving
- The model evolution calculus as a first-order DPLL method
- Superposition with equivalence reasoning and delayed clause normal form transformation
- 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
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)
