Skip navigation
Skip navigation

Finite Quantification in Hierarchic Theorem Proving

Baumgartner, Peter; Bax, Joshua; Waldmann, Uwe

Description

Many applications of automated deduction require reasoning in first-order logic modulo background theories, in particular some form of integer arithmetic. A major unsolved research challenge is to design theorem provers that are "reasonably complete" even in the presence of free function symbols ranging into a background theory sort. In this paper we consider the case when all variables occurring below such function symbols are quantified over a finite subset of their domains. We present a...[Show more]

CollectionsANU Research Publications
Date published: 2014
Type: Conference paper
URI: http://hdl.handle.net/1885/67001
Source: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
DOI: 10.1007/978-3-319-08587-6_11

Download

File Description SizeFormat Image
01_Baumgartner_Finite_Quantification_in_2014.pdf314.79 kBAdobe PDF    Request a copy


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

Updated:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator