Journal article
Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
Automated Reasoning, Vol.12166, pp.141-160
05/30/2020
DOI: 10.1007/978-3-030-51074-9_9
Abstract
The abduction problem in logic asks whether there exists a formula that is consistent with a given set of axioms and, together with these axioms, suffices to entail a given goal. We propose an approach for solving this problem that is based on syntax-guided enumeration. For scalability, we use a novel procedure that incrementally constructs a solution in disjunctive normal form that is built from enumerated formulas. The procedure can be configured to generate progressively weaker and simpler solutions over the course of a run of the procedure. Our approach is fully general and can be applied over any background logic that is handled by the underlying SMT solver in our approach. Our experiments show our approach compares favorably with other tools for abductive reasoning.
Details
- Title: Subtitle
- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis
- Creators
- Andrew Reynolds - University of IowaHaniel Barbosa - Universidade Federal de Minas GeraisDaniel Larraz - University of IowaCesare Tinelli - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Automated Reasoning, Vol.12166, pp.141-160
- DOI
- 10.1007/978-3-030-51074-9_9
- eISBN
- 9783030510749; 3030510743
- ISSN
- 0302-9743
- eISSN
- 1611-3349
- Language
- English
- Date published
- 05/30/2020
- Academic Unit
- Computer Science
- Record Identifier
- 9984259428002771
Metrics
12 Record Views