Scalable algorithms for abduction via enumerative syntax-guided synthesis

DOI10.1007/978-3-030-51074-9_9MaRDI QIDQ2096443zbMATH OpenOpenAlexFDO

Authors Andrew Reynolds, Haniel Barbosa, Daniel Larraz, Cesare Tinelli

Publication date 9 November 2022

Full work available at URL https://doi.org/10.1007/978-3-030-51074-9_9

Mathematics Subject Classification ID

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

Recommendations

• Abduction from logic programs: Semantics and complexity
• An abductive framework for extended logic programming
• Complexity results for abductive logic programming
• Abductive Logic Programming
• Scalable reasoning by abstraction beyond DL-Lite
• scientific article; zbMATH DE number 898328
• scientific article; zbMATH DE number 2077154
• Reasoning with higher-order abstract syntax and contexts: a comparison
• Parameterised complexity of abduction in Schaefer's framework

Cites work

• A generic framework for implicate generation modulo theories
• A mathematical introduction to logic.
• Abductive Inference
• Automated inference of library specifications for source-sink property verification
• Compositional shape analysis by means of bi-abduction
• Computing small unsatisfiable cores in satisfiability modulo theories
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Extending SMT solvers to higher-order logic
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Ilinva: using abduction to generate loop invariants
• Maximal specification synthesis
• Scaling enumerative program synthesis via divide and conquer
• Syntax-guided rewrite rule enumeration for SMT solvers
• Synthesis of circular compositional program proofs via abduction
• The implicit hitting set approach to solve combinatorial optimization problems with an application to multigenome alignment

Cited in

(4)

• Syntax-guided synthesis with quantitative syntactic objectives
• Theorem proving as constraint solving for coherent logic with function symbols
• Automated completion of statements and proofs in synthetic geometry: an approach based on constraint solving
• An interactive SMT tactic in Coq using abductive reasoning

Describes a project that uses

Uses Software

• CVC4
• z3

This page was built for publication: Scalable algorithms for abduction via enumerative syntax-guided synthesis

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