Skip navigation
Skip navigation

The hyper Tableaux calculus with equality and an application to finite model computation

Baumgartner, Peter; Furbach, Ulrich; Pelzer, Bjorn

Description

In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this article we show how to integrate a modern treatment of equality in the hyper tableau calculus. It is based on splitting of positive clauses and an adapted version of the superposition inference rule, where equations used for superposition are drawn (only) from a set of positive unit clauses, and superposition inferences into positive literals is restricted into (positive) unit...[Show more]

CollectionsANU Research Publications
Date published: 2008
Type: Journal article
URI: http://hdl.handle.net/1885/55021
Source: Journal of Logic and Computation
DOI: 10.1093/logcom/exn061

Download

File Description SizeFormat Image
01_Baumgartner_The_hyper_Tableaux_calculus_2008.pdf458.96 kBAdobe PDF    Request a copy


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

Updated:  12 November 2018/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator