Extending a high-performance prover to higher-order logic
From MaRDI portal
Publication:6536126
DOI10.1007/978-3-031-30820-8_10zbMATH Open1547.68819MaRDI QIDQ6536126
Petar Vukmirović, Stephan Schulz, Jasmin Christian Blanchette
Publication date: 5 April 2024
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Superposition for \(\lambda\)-free higher-order logic
- An introduction to mathematical logic and type theory: To truth through proof.
- The locally nameless representation
- LEO-II and Satallax on the Sledgehammer test bench
- Superposition for full higher-order logic
- A combinator-based superposition calculus for higher-order logic
- Lash 1.0 (system description)
- Extending SMT solvers to higher-order logic
- Restricted combinatory unification
- Faster, higher, stronger: E 2.3
- Extensional higher-order paramodulation in Leo-III
- Reviewing the classical and the de Bruijn notation for \(\lambda\)-calculus and pure type systems
- Satallax: An Automatic Higher-Order Prover
- Fingerprint Indexing for Paramodulation and Rewriting
- There Is No Best $$\beta $$ -Normalization Strategy for Higher-Order Reasoners
- A Linear Spine Calculus
- Simple and Efficient Clause Subsumption with Feature Vector Indexing
- The 10th IJCAR automated theorem proving system competition – CASC-J10
- Hammering towards QED
- Sine Qua Non for Large Theory Reasoning
- Superposition with lambdas
- Making higher-order superposition work
- Seventeen provers under the hammer
This page was built for publication: Extending a high-performance prover to higher-order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536126)
