Machine learning guidance for connection tableaux
From MaRDI portal
Publication:2031418
DOI10.1007/s10817-020-09576-7OpenAlexW3083107390WikidataQ108482096 ScholiaQ108482096MaRDI QIDQ2031418
Josef Urban, Michael Färber, Cezary Kaliszyk
Publication date: 9 June 2021
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-020-09576-7
Related Items (3)
The role of entropy in guiding a connection prover ⋮ Eliminating models during model elimination ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures
Uses Software
Cites Work
- MizAR 40 for Mizar 40
- A learning-based fact selector for Isabelle/HOL
- Automated reasoning with analytic tableaux and related methods. 20th international conference, TABLEAUX 2011, Bern, Switzerland, July 4--8, 2011. Proceedings
- MPTP-motivation, implementation, first experiments
- Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
- The ILTP problem library for intuitionistic logic
- On connections and higher-order logic
- Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
- Lightweight relevance filtering for machine-generated resolution problems
- A structure-preserving clause form translation
- Game-theoretical semantics: Insights and prospects
- SETHEO: A high-performance theorem prover
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- The CADE-14 ATP system competition
- IeanCOP: lean connection-based theorem proving
- Connection methods in linear logic and proof nets construction
- A vision for automated deduction rooted in the connection method
- lean\(T^ AP\): Lean tableau-based deduction
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- HOL(y)Hammer: online ATP service for HOL Light
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- ENIGMA: efficient learning-based inference guiding machine
- Monte Carlo tableau proof search
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- nanoCoP: A Non-clausal Connection Prover
- Selecting the Selection
- Internal Guidance for Satallax
- System Description: E 1.8
- Automated and Human Proofs in General Mathematics: An Initial Comparison
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- A Non-clausal Connection Calculus
- MaLeCoP Machine Learning Connection Prover
- HOL Light: An Overview
- A Brief Overview of Agda – A Functional Language with Dependent Types
- MleanCoP: A Connection Prover for First-Order Modal Logic
- System Description: E.T. 0.1
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)
- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
- A Short Presentation of Coq
- A Brief Overview of HOL4
- The Isabelle Framework
- Restricting backtracking in connection calculi
- Matings in matrices
- The 8th IJCAR automated theorem proving system competition – CASC-J8
- Deep Network Guided Proof Search
- Hammering towards QED
- Sine Qua Non for Large Theory Reasoning
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- MaSh: Machine Learning for Sledgehammer
- Automated Reasoning with Analytic Tableaux and Related Methods
- Mechanical Theorem-Proving by Model Elimination
- Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Machine learning guidance for connection tableaux
