Superposition with structural induction

DOI10.1007/978-3-319-66167-4_10zbMATH Open1496.68365OpenAlexW2749302087MaRDI QIDQ1687553FDOQ1687553

Authors: Simon Cruanes 

Publication date: 4 January 2018

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

Recommendations

• Induction with generalization in superposition reasoning
• Superposition for full higher-order logic
• Combining superposition and induction: a practical realization
• Making higher-order superposition work
• Making higher-order superposition work

Mathematics Subject Classification ID

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

Cited In (22)

• Restricted combinatory unification
• Superposition with lambdas
• Title not available (Why is that?)
• Superposition with lambdas
• Title not available (Why is that?)
• Quantifier-free induction for lists
• Title not available (Why is that?)
• Inductive benchmarks for automated reasoning
• Superposition with first-class booleans and inprocessing clausification
• Induction with generalization in superposition reasoning
• Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
• Induction in saturation-based proof search
• 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
• Getting saturated with induction
• A Polymorphic Vampire
• Induction and Skolemization in saturation theorem proving
• Combining induction and saturation-based theorem proving

Uses Software

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

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)