Skip navigation
Skip navigation

Disproving in First-Order Logic with Definitions, Arithmetic and Finite Domains

Bax, Joshua


This thesis explores several methods which enable a first-order reasoner to conclude satisfiability of a formula modulo an arithmetic theory. The most general method requires restricting certain quantifiers to range over finite sets; such assumptions are common in the software verification setting. In addition, the use of first-order reasoning allows for an implicit representation of those finite sets, which can avoid scalability problems that affect other...[Show more]

CollectionsOpen Access Theses
Date published: 2017
Type: Thesis (PhD)
DOI: 10.25911/5d666b238d5ba


File Description SizeFormat Image
Bax Thesis 2017.pdf986.27 kBAdobe PDFThumbnail

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator