Faster, higher, stronger: E 2.3

DOI10.1007/978-3-030-29436-6_29OpenAlexW2969992190MaRDI QIDQ2305435

Simon Cruanes, Petar Vukmirović, Stephan Schulz

Publication date: 10 March 2020

Full work available at URL: https://hal.inria.fr/hal-02296188/file/sde2_3.pdf

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (35)

A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Fast and slow enigmas and parental guidance ⋮ Vampire with a brain is a good ITP hammer ⋮ Teaching Automated Theorem Proving by Example: PyRes 1.2 ⋮ Make E Smart Again (Short Paper) ⋮ A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (System Description) ⋮ The \textsf{nanoCoP 2.0} connection provers for classical, intuitionistic and modal logics ⋮ Eliminating models during model elimination ⋮ The CADE-28 Automated Theorem Proving System Competition – CASC-28 ⋮ Craig interpolation with clausal first-order tableaux ⋮ Unnamed Item ⋮ A strict constrained superposition calculus for graphs ⋮ The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ CICM'22 system entries ⋮ Getting saturated with induction ⋮ Solving modal logic problems by translation to higher-order logic ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Neural precedence recommender ⋮ Improving ENIGMA-style clause selection while learning from history ⋮ Twee: an equational theorem prover ⋮ E Theorem Prover ⋮ Subsumption demodulation in first-order theorem proving ⋮ Layered clause selection for theory reasoning (short paper) ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ Local is best: efficient reductions to modal logic \textsf{K} ⋮ Local reductions for the modal cube ⋮ Guiding an automated theorem prover with neural rewriting ⋮ SAT-Inspired Eliminations for Superposition

Uses Software

• SMT-LIB
• TPTP
• Why3
• PicoSAT
• StarExec
• DISCOUNT
• Proofwatch

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• ProofWatch: watchlist guidance for large theories in E
• Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving
• System Description: E 1.8
• The TPTP Typed First-Order Form with Arithmetic
• Fingerprint Indexing for Paramodulation and Rewriting
• Playing with AVATAR
• Using the TPTP Language for Writing Derivations and Finite Interpretations
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• The 8th IJCAR automated theorem proving system competition – CASC-J8
• Simple and Efficient Clause Subsumption with Feature Vector Indexing
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• Hammering towards QED
• Sine Qua Non for Large Theory Reasoning

This page was built for publication: Faster, higher, stronger: E 2.3