Sine Qua Non for Large Theory Reasoning

DOI10.1007/978-3-642-22438-6_23zbMath1341.68189OpenAlexW41512512MaRDI QIDQ5200032

Andrei Voronkov, Kryštof Hoder

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_23

Mathematics Subject Classification ID

Related Items

Improving stateful premise selection with transformers, MizAR 40 for Mizar 40, Vampire with a brain is a good ITP hammer, Automatic Proof and Disproof in Isabelle/HOL, Eliminating models during model elimination, Automated Reasoning in the Wild, System Description: E.T. 0.1, A learning-based fact selector for Isabelle/HOL, Hammer for Coq: automation for dependent type theory, Random Forests for Premise Selection, ATP and presentation service for Mizar formalizations, Learning-assisted theorem proving with millions of lemmas, The CADE-26 automated theorem proving system competition – CASC-26, Hierarchical invention of theorem proving strategies, The CADE-27 Automated theorem proving System Competition – CASC-27, MaLeCoP Machine Learning Connection Prover, HOL(y)Hammer: online ATP service for HOL Light, Machine learning guidance for connection tableaux, Extending Sledgehammer with SMT Solvers, Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving, Internal Guidance for Satallax, Names are not just sound and smoke: word embeddings for axiom selection, Faster, higher, stronger: E 2.3, Extending Sledgehammer with SMT solvers, Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\), Premise selection for mathematics by corpus analysis and kernel methods

Uses Software

• MPTP 0.2
• VAMPIRE
• TPTP
• Mizar
• MML
• MaLARea
• SInE
• SRASS

Cites Work

• A relevance restriction strategy for automated deduction
• MPTP 0.2: Design, implementation, and initial experiments
• Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
• Lightweight relevance filtering for machine-generated resolution problems
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance
• The CADE-22 automated theorem proving system competition – CASC-22
• SRASS - A Semantic Relevance Axiom Selection System
• Interpolation and Symbol Elimination in Vampire
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library