Extending SMT solvers to higher-order logic

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

Mathematics Subject Classification ID

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

• LEO-II
• Isabelle/HOL
• SMT-LIB
• TPTP
• SIMPLIFY
• Satallax
• Sledgehammer
• veriT
• CVC4
• E Theorem Prover
• CoqHammer

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