Premise Selection in the Naproche System

DOI10.1007/978-3-642-14203-1_37zbMath1291.68336OpenAlexW1596298944MaRDI QIDQ5747782

Daniel Kühlwein, Marcos Cramer, Peter Koepke, Bernhard Schröder

Publication date: 14 September 2010

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_37

zbMATH Keywords

automated theorem provingformal mathematicsaxiom selection

Mathematics Subject Classification ID

Related Items

A fully automatic theorem prover with human-style output ⋮ Beautiful formalizations in Isabelle/Naproche ⋮ Premise Selection in the Naproche System ⋮ Parsing and Disambiguation of Symbolic Mathematics in the Naproche System ⋮ The Isabelle/Naproche natural language proof assistant

Uses Software

• TPTP
• Metis_
• Isar
• SAD
• E Theorem Prover
• MaLARea
• Naproche

Cites Work

• Lightweight relevance filtering for machine-generated resolution problems
• Gazing: An approach to the problem of definition and lemma use
• The language of mathematics. A linguistic and philosophical investigation
• 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
• SRASS - A Semantic Relevance Axiom Selection System
• System for Automated Deduction (SAD): A Tool for Proof Verification
• Premise Selection in the Naproche System
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item