Extending SMT solvers to higher-order logic
From MaRDI portal
Publication:2305406
DOI10.1007/978-3-030-29436-6_3OpenAlexW2969891771MaRDI QIDQ2305406
Haniel Barbosa, Andrew Reynolds, Cesare Tinelli, Clark Barrett, Daniel El Ouraoui
Publication date: 10 March 2020
Full work available at URL: https://doi.org/10.1007/978-3-030-29436-6_3
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Improving automation for higher-order proof steps, Extensional higher-order paramodulation in Leo-III, The CADE-27 Automated theorem proving System Competition – CASC-27, Superposition with lambdas, Making higher-order superposition work, Making higher-order superposition work, Reliable reconstruction of fine-grained proofs in a proof assistant, Extending SMT solvers to higher-order logic, Scalable algorithms for abduction via enumerative syntax-guided synthesis, A combinator-based superposition calculus for higher-order logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The higher-order prover \textsc{Leo}-II
- Translation of Turner combinators in O(n log n) space
- Fast congruence closure and extensions
- The CADE-14 ATP system competition
- Isabelle/HOL. A proof assistant for higher-order logic
- Hammer for Coq: automation for dependent type theory
- Superposition with structural induction
- Superposition for \(\lambda\)-free higher-order logic
- The higher-order prover Leo-III
- LEO-II and Satallax on the Sledgehammer test bench
- Extending SMT solvers to higher-order logic
- Revisiting enumerative instantiation
- Translating higher-order clauses to first-order clauses
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Internal Guidance for Satallax
- Satallax: An Automatic Higher-Order Prover
- Congruence Closure with Free Variables
- Simplify: a theorem prover for program checking
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Fast Decision Procedures Based on Congruence Closure
- Variations on the Common Subexpression Problem
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Quantifier Instantiation Techniques for Finite Model Finding in SMT
- Hammering towards QED
- Resolution in type theory
- Sledgehammer: Judgement Day
- Completeness in the theory of types
