Model elimination and connection tableau procedures
From MaRDI portal
Recommendations
- A disjunctive positive refinement of model elimination and its application to subsumption deletion
- Model elimination without contrapositives
- scientific article; zbMATH DE number 517000
- scientific article; zbMATH DE number 1552524
- A more efficient tableaux procedure for simultaneous search for refutations and finite models
Cited in
(25)- A disjunctive positive refinement of model elimination and its application to subsumption deletion
- Machine learning guidance for connection tableaux
- Set of support, demodulation, paramodulation: a historical perspective
- \textsf{lazyCoP}: lazy paramodulation meets neurally guided search
- The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics
- Eliminating models during model elimination
- Towards a unified model of search in theorem-proving: subgoal-reduction strategies
- A sequent-style model elimination strategy and a positive refinement
- Craig interpolation with clausal first-order tableaux
- Encoding first order proofs in SMT
- Semantically-guided goal-sensitive reasoning: model representation
- A Non-clausal Connection Calculus
- Specifying and verifying organizational security properties in first-order logic
- Efficient Low-Level Connection Tableaux
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- scientific article; zbMATH DE number 1748583 (Why is no real title available?)
- From Schütte’s Formal Systems to Modern Automated Deduction
- Prolog Technology Reinforcement Learning Prover
- Range-restricted and Horn interpolation through clausal tableaux
- On structures of sign-boundary and diagonal vacancy-type standard contradictions
- Constraint learning for non-confluent proof search
- Finding connections via satisfiability solving
- SAD as a mathematical assistant -- how should we go from here to there?
- A sound framework for \(\delta\)-rule variants in free-variable semantic tableaux
- Connection tableaux with lazy paramodulation
This page was built for publication: Model elimination and connection tableau procedures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751380)
