Portfolio theorem proving and prover runtime prediction for geometry
DOI10.1007/s10472-018-9598-6zbMath1431.68123OpenAlexW2892064985WikidataQ129286195 ScholiaQ129286195MaRDI QIDQ2631959
Mladen Nikolić, Predrag Janičić, Zoltán Kovács, Vesna Marinković
Publication date: 16 May 2019
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-018-9598-6
Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Elementary problems in Euclidean geometries (51M04) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Automated theorem proving in GeoGebra: current achievements
- MaLeS: a framework for automatic tuning of automated theorem provers
- The area method. A recapitulation
- Algorithm runtime prediction: methods \& evaluation
- Learning from planner performance
- A self-adaptive multi-engine solver for quantified Boolean formulas
- Linear regression.
- Isabelle/HOL. A proof assistant for higher-order logic
- Hammer for Coq: automation for dependent type theory
- meSAT: multiple encodings of CSP to SAT
- Premise selection for mathematics by corpus analysis and kernel methods
- A Singular web service for geometric computations
- Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
- Finding proofs in Tarskian geometry
- Geometry constructions language
- Giac and GeoGebra – Improved Gröbner Basis Computations
- Internal Guidance for Satallax
- Towards Understanding Triangle Construction Problems
- SUNNY: a Lazy Portfolio Approach for Constraint Solving
- Random Forests for Premise Selection
- MaLeCoP Machine Learning Connection Prover
- The Sequential Parameter Optimization Toolbox
- A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
- Community Branching for Parallel Portfolio SAT Solvers
- Computer Theorem Proving for Verifiable Solving of Geometric Construction Problems
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- Online Estimation of SAT Solving Runtime
- Triangle Constructions with Three Located Points
- An introduction to geometry expert
- Machine Proofs in Geometry
- Automatic Verification of Regular Constructions in Dynamic Geometry Systems
- Linear Statistical Inference and its Applications
- GCLC — A Tool for Constructive Euclidean Geometry and More Than That
- On Information and Sufficiency
- Principles and Practice of Constraint Programming – CP 2004
- Automated Deduction in Geometry
- The elements of statistical learning. Data mining, inference, and prediction
This page was built for publication: Portfolio theorem proving and prover runtime prediction for geometry