scientific article; zbMATH DE number 1765699
From MaRDI portal
Publication:4539640
Recommendations
Cited in
(17)- Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
- Theorem proving with bounded rigid \(E\)-unification
- Differential dynamic logic for hybrid systems
- Incremental variable splitting
- Liberalized variable splitting
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Superposition-based equality handling for analytic tableaux
- Depth-first proof search without backtracking for free-variable clausal tableaux
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- Free-variable tableaux for monotonic preorders
- KeY: A Formal Method for Object-Oriented Systems
- Logics in Artificial Intelligence
- The model evolution calculus as a first-order DPLL method
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- Incremental theory reasoning methods for semantic tableaux
- Goal-sensitive reasoning with disconnection tableaux
- Satisfiability solving and model generation for quantified first-order logic formulas
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 Q4539640)
