System Description: E.T. 0.1

DOI10.1007/978-3-319-21401-6_27zbMath1465.68286OpenAlexW1413051680WikidataQ108482217 ScholiaQ108482217MaRDI QIDQ3454109

Jiří Vyskočil, Stephan Schulz, Josef Urban, Cezary Kaliszyk

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_27

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ A multi-clause dynamic deduction algorithm based on standard contradiction separation rule ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Machine learning guidance for connection tableaux ⋮ Internal Guidance for Satallax

Uses Software

• MPTP
• MPTP 0.2
• OTTER
• VAMPIRE
• TPTP
• Mizar
• MML
• MaSh
• E Theorem Prover
• Flyspeck
• HOLyHammer
• SigmaKEE
• BliStr
• SRASS

Cites Work

• Unnamed Item
• MizAR 40 for Mizar 40
• MPTP-motivation, implementation, first experiments
• MPTP 0.2: Design, implementation, and initial experiments
• Matrix interpretations for proving termination of term rewriting
• Lightweight relevance filtering for machine-generated resolution problems
• The IJCAR ATP system competition
• HOL(y)Hammer: online ATP service for HOL Light
• Premise selection for mathematics by corpus analysis and kernel methods
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• System Description: E 1.8
• AVATAR: The Architecture for First-Order Theorem Provers
• Lemmatization for Stronger Reasoning in Large Theories
• OTTER Proofs in Tarskian Geometry
• Minimal and complete word unification
• An application of automated reasoning in natural language question answering
• SRASS - A Semantic Relevance Axiom Selection System
• A Decision Algorithm for Stratified Context Unification
• The 481 Ways to Split a Clause and Deal with Propositional Variables
• Hammering towards QED
• Sine Qua Non for Large Theory Reasoning
• MaSh: Machine Learning for Sledgehammer
• Evaluation of Automated Theorem Proving on the Mizar Mathematical Library

This page was built for publication: System Description: E.T. 0.1