Skip navigation
Skip navigation

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

Bax, Joshua

Description

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)
URI: http://hdl.handle.net/1885/138339

Download

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:  23 August 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator