onr:"swepub:oai:research.chalmers.se:cfde9b4f-983e-4ec2-85c1-f96c78da8823"
Search: onr:"swepub:oai:research.chalmers.se:cfde9b4f-983e-4ec2-85c1-f96c78da8823" > Interpolation Syste...
- 1 of 1
- Previous record
- Next record
- To hitlist
Interpolation Systems for Ground Proofs in Automated Deduction: a Survey
-
- Bonacina, M.P. (author)
- Universita degli Studi di Verona,Verona University
-
- Johansson, Moa, 1981 (author)
- Chalmers tekniska högskola,Chalmers University of Technology
- (creator_code:org_t)
- 2015-03-20
- 2015
- English.
- In: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 54:4, s. 353-390
- Journal article (peer-reviewed)
Abstract
Subject headings
Close
- Interpolation is a deductive technique applied in program analysis and verification: for example, it is used to compute over-approximations of images or refine abstractions. An interpolation system takes a refutation and extracts an interpolant by building it inductively from partial interpolants. We survey color-based interpolation systems for ground proofs produced by key inference engines of state-of-the-art solvers: DPLL for propositional logic, equality sharing for combination of convex theories, and DPLL((Formula presented.)) for SMT-solving. Since color-based interpolation systems use colors to track symbols in proofs, equality is problematic, because replacement of equals by equals mixes symbols and therefore colors. We analyze interpolation in the presence of equality, and we demonstrate the color-based approach by giving a complete interpolation system for ground proofs by superposition.
Subject headings
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
Keyword
- Satisfiability modulo theories
- Decision procedures
- Theory combination
- Interpolation systems
Publication and Content Type
- art (subject category)
- ref (subject category)
Find in a library
- Journal of Automated Reasoning (Search for host publication in LIBRIS)
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Bonacina, M.P.
- Johansson, Moa, ...
- About the subject
-
- ENGINEERING AND TECHNOLOGY
- ENGINEERING AND ...
- and Electrical Engin ...
- and Embedded Systems
- Articles in the publication
- Journal of Autom ...
- By the university
- Chalmers University of Technology
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
