Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Quantifiers and Theories: A Lazy Approach
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2019 (English)Doctoral thesis, monograph (Other academic)
Description
Abstract [en]

In this thesis we study Automated Theorem Proving (ATP) as well as Satisfiability Modulo Theories (SMT) and present lazy strategies for improving reasoning within these areas. A lazy strategy works by simplifying a problem, and gradually refines the abstraction only when necessary. Often, a solution can be found without solving the full problem, saving valuable resources. We formulate our contributions within two key challenges in ATP and SMT: theory and quantifier reasoning.Many problems need first-order reasoning modulo a theory, i.e., reasoning where symbols in formulas are interpreted according to some background theory. In software verification, which often involves conditions over machine arithmetic, bit-vectors as well as floating-point numbers play an important role. Finding methods for how to reason with these theories in an efficient manner is therefore an important task. In this thesis we present a lazy method for handling bit-vector constraints as well as bit-vector interpolation, which improves performance and produces simpler interpolants. Moreover, a modular approximation framework is described, which allows for high-level description of lazy strategies applicable to a multitude of theories. Such a strategy is combined with a back-end, creating an approximating SMT solver. We use floating-point arithmetic as an illustrating use case, showing how the lazy strategy can improve the overall efficiency.The quantifier is a language construct which allows for making statements about one or all objects of some universe. However, with great power comes great cost - reasoning with quantifiers is very hard. Many decision problems involving quantifiers are not decidable, e.g., validity of first-order logic. Intricate strategies are needed to handle formulas with quantifiers, especially in combination with theory reasoning. We present a new restricted form of unification, by lazy expansion of the domain of substitution, as well as efficient procedures to solve it. This is incorporated into a complete and sound sequent calculus for the combination of the theory of equality and quantifiers.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2019. , p. 214
Series
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 139
Keywords [en]
Automated Reasoning, Automated Theorem Proving, SMT, Unification
National Category
Computer Sciences
Research subject
Computer Science with specialization in Embedded Systems
Identifiers
URN: urn:nbn:se:uu:diva-395985ISBN: 978-91-513-0805-0 (print)OAI: oai:DiVA.org:uu-395985DiVA, id: diva2:1366312
Public defence
2019-12-18, ITC/2446, Lägerhyddsvägen 2, Uppsala, 09:00 (English)
Opponent
Supervisors
Available from: 2019-11-22 Created: 2019-10-29 Last updated: 2019-11-22

Open Access in DiVA

fulltext(1301 kB)44 downloads
File information
File name FULLTEXT01.pdfFile size 1301 kBChecksum SHA-512
defc8afcd00cd48f0cddfc8445d581dedefbbc7dac1964298ba70297cacd71b594b96a24d4dc42c5f8c35112563289713bc2e23242cf217336edc5ff875b5ea0
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Backeman, Peter
By organisation
Division of Computer SystemsComputer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 44 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 107 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf