DagSemProc.07401.6.pdf
- Filesize: 254 kB
- 22 pages
Document
Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
Authors
-
Part of:
Volume:
Dagstuhl Seminar Proceedings, Volume 7401
Series: Dagstuhl Seminar Proceedings (DagSemProc) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2007-11-29
Cite As Get BibTex
Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs. Local Theory Extensions, Hierarchical Reasoning and Applications to Verification. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)
https://doi.org/10.4230/DagSemProc.07401.6
Abstract
Many problems occurring in verification can be reduced to proving the satisfiability of conjunctions of literals in a background theory. This can be a concrete theory (e.g. the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories. We present some new results on hierarchical and modular reasoning in complex theories, as well as several examples of application domains in which efficient reasoning is possible. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of local theory extension.
Subject Classification
Keywords
- Automated reasoning
- Combinations of decision procedures
- Verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads