Superposition with structural induction
From MaRDI portal
Publication:1687553
DOI10.1007/978-3-319-66167-4_10zbMath1496.68365OpenAlexW2749302087MaRDI QIDQ1687553
Publication date: 4 January 2018
Full work available at URL: https://hal.inria.fr/hal-02062459/file/frocos_17_paper.pdf
Related Items (19)
Inductive benchmarks for automated reasoning ⋮ Theory exploration powered by deductive synthesis ⋮ A Polymorphic Vampire ⋮ Unnamed Item ⋮ Machine Learning for Inductive Theorem Proving ⋮ Getting saturated with induction ⋮ Unnamed Item ⋮ Superposition with lambdas ⋮ Superposition with lambdas ⋮ Combining induction and saturation-based theorem proving ⋮ Integer induction in saturation ⋮ Superposition with first-class booleans and inprocessing clausification ⋮ Extending SMT solvers to higher-order logic ⋮ Restricted combinatory unification ⋮ Induction in saturation-based proof search ⋮ Unnamed Item ⋮ Unprovability results for clause set cycles ⋮ Induction and Skolemization in saturation theorem proving ⋮ SAT-Inspired Eliminations for Superposition
Uses Software
This page was built for publication: Superposition with structural induction
