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 AsGet 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
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.
Keywords
- Automated reasoning
- Combinations of decision procedures
- Verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads