scientific article; zbMATH DE number 1552532
From MaRDI portal
Publication:4524792
Recommendations
Cited in
(50)- A superposition oriented theorem prover
- The equational part of proofs by structural induction
- Horn equational theories and paramodulation
- Equational theorem proving modulo
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Pay-as-you-go consequence-based reasoning for the description logic \(\mathcal{SROIQ} \)
- Blocking and other enhancements for bottom-up model generation methods
- The model evolution calculus as a first-order DPLL method
- Resolution with order and selection for hybrid logics
- Superposition with equivalence reasoning and delayed clause normal form transformation
- Paramodulation-based theorem proving
- Equality reasoning in sequent-based calculi
- Combining superposition, sorts and splitting
- scientific article; zbMATH DE number 1670742 (Why is no real title available?)
- Selecting the selection
- Computing All Implied Equalities via SMT-Based Partition Refinement
- Automated reasoning building blocks
- Inferring Congruence Equations Using SAT
- Paramodulation with non-monotonic orderings and simplification
- I-terms in ordered resolution and superposition calculi: retrieving lost completeness
- scientific article; zbMATH DE number 3986667 (Why is no real title available?)
- scientific article; zbMATH DE number 1300967 (Why is no real title available?)
- scientific article; zbMATH DE number 1303344 (Why is no real title available?)
- scientific article; zbMATH DE number 1324442 (Why is no real title available?)
- scientific article; zbMATH DE number 1348470 (Why is no real title available?)
- A Tableaux Method for Systematic Simultaneous Search for Refutations and Models using Equational Problems
- Model evolution with equality -- revised and implemented
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- A combined superposition and model evolution calculus
- Harald Ganzinger's legacy: contributions to logics and programming
- First-order resolution methods for modal logics
- Quantifier Elimination and Provers Integration
- Superposition and Model Evolution Combined
- The anatomy of Equinox -- an extensible automated reasoning tool for first-order logic and beyond (talk abstract)
- Computer Science Logic
- Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case
- Model-theoretic methods in combined constraint satisfiability
- iProver-Eq: An Instantiation-Based Theorem Prover with Equality
- Superposition with equivalence reasoning and delayed clause normal form transformation.
- A comprehensive framework for saturation theorem proving
- Connection calculus theorem proving with multiple built-in theories
- A comprehensive framework for saturation theorem proving
- Equational Theorem Proving for Clauses over Strings
- Positive deduction modulo regular theories
- Equational theorem proving for clauses over strings
- Rewriting and inductive reasoning
- Reducibility constraints in superposition
- Theorem-proving with resolution and superposition
- The disconnection tableau calculus
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)
