Eliminating models during model elimination
From MaRDI portal
Publication:2142079
DOI10.1007/978-3-030-86059-2_15OpenAlexW3197014198MaRDI QIDQ2142079
Publication date: 25 May 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-86059-2_15
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Four decades of {\textsc{Mizar}}. Foreword
- MPTP 0.2: Design, implementation, and initial experiments
- Limited resource strategy in resolution theorem proving
- Machine learning guidance for connection tableaux
- SAT competition 2020
- Faster, higher, stronger: E 2.3
- Reducing higher-order theorem proving to a sequence of SAT problems
- Premise selection for mathematics by corpus analysis and kernel methods
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- nanoCoP: A Non-clausal Connection Prover
- Finding Finite Models in Multi-sorted First-Order Logic
- AVATAR: The Architecture for First-Order Theorem Provers
- MleanCoP: A Connection Prover for First-Order Modal 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)
- Restricting backtracking in connection calculi
- Encoding First Order Proofs in SAT
- Theorem Proving via General Matings
- GRASP: a search algorithm for propositional satisfiability
- Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
- Prolog Technology Reinforcement Learning Prover
- Sine Qua Non for Large Theory Reasoning
- Logic programming with satisfiability
- Automated Deduction – CADE-19
