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 (26)

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

This page was built for publication: Sine Qua Non for Large Theory Reasoning