Superposition with structural induction

DOI10.1007/978-3-319-66167-4_10MaRDI QIDQ1687553zbMATH OpenOpenAlexFDO

Authors Simon Cruanes

Publication date 4 January 2018

Full work available at URL https://hal.inria.fr/hal-02062459/file/frocos_17_paper.pdf

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Superposition for full higher-order logic
• Combining superposition and induction: a practical realization
• Making higher-order superposition work
• Making higher-order superposition work

Cited in

(22)

• Restricted combinatory unification
• Superposition with lambdas
• scientific article; zbMATH DE number 7350767 (Why is no real title available?)
• Combining superposition and induction: a practical realization
• Superposition with lambdas
• scientific article; zbMATH DE number 7471678 (Why is no real title available?)
• Quantifier-free induction for lists
• Inductive benchmarks for automated reasoning
• Superposition with first-class booleans and inprocessing clausification
• Induction in saturation-based proof search
• Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
• Extending SMT solvers to higher-order logic
• Theory exploration powered by deductive synthesis
• Unprovability results for clause set cycles
• Machine Learning for Inductive Theorem Proving
• Integer induction in saturation
• SAT-Inspired Eliminations for Superposition
• Clause set cycles and induction
• Getting saturated with induction
• A Polymorphic Vampire
• Induction and Skolemization in saturation theorem proving
• Combining induction and saturation-based theorem proving

Describes a project that uses

Uses Software

• Zipperposition
• AVATAR
• InKa
• E Theorem Prover
• HipSpec
• QuickCheck
• z3
• TPTP
• SPASS
• VAMPIRE
• ACL2

This page was built for publication: Superposition with structural induction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687553)