GRUNGE: a grand unified ATP challenge
From MaRDI portal
Publication:2305410
DOI10.1007/978-3-030-29436-6_8OpenAlexW3102235081WikidataQ108482114 ScholiaQ108482114MaRDI QIDQ2305410
Cezary Kaliszyk, Thibault Gauthier, Josef Urban, Geoff Sutcliffe, Chad Edward Brown
Publication date: 10 March 2020
Full work available at URL: https://arxiv.org/abs/1903.02539
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
A Polymorphic Vampire, \( \alpha \)-paramodulation method for a lattice-valued logic \(L_nF(X)\) with equality, Extensional higher-order paramodulation in Leo-III, The 11th IJCAR automated theorem proving system competition – CASC-J11, Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support, The CADE-27 Automated theorem proving System Competition – CASC-27, The 10th IJCAR automated theorem proving system competition – CASC-J10
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14--19, 2013. Proceedings
- The CADE-14 ATP system competition
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- The higher-order prover Leo-III
- TacticToe: learning to prove with tactics
- Contradiction separation based dynamic multi-clause synergized automated deduction
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Premise selection for mathematics by corpus analysis and kernel methods
- Translating higher-order clauses to first-order clauses
- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
- System Description: E 1.8
- E-Matching with Free Variables
- The TPTP Typed First-Order Form with Arithmetic
- Satallax: An Automatic Higher-Order Prover
- A Focused Sequent Calculus for Higher-Order Logic
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- A Brief Overview of HOL4
- TacticToe: Learning to Reason with HOL4 Tactics
- Optimizing proof search in model elimination
- Hierarchic Superposition with Weak Abstraction
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- The 9th IJCAR Automated Theorem Proving System Competition – CASC-J9
- Hammering towards QED
- Experimenting with Deduction Modulo
- Encoding Monomorphic and Polymorphic Types
- CakeML
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Fast LCF-Style Proof Reconstruction for Z3
