UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

A resolution framework for finitely-valued first-order logics

O'Hearn, PW; Stachniak, Z; (1992) A resolution framework for finitely-valued first-order logics. Journal of Symbolic Computation , 13 (3) pp. 235-254. 10.1016/S0747-7171(10)80002-1.

Full text not available from this repository.

Abstract

In this paper we propose a resolution proof framework on the basis of which automated proof systems for finitely-valued first-order logics (FFO logics) can be introduced and studied. We define the notion of a first-order resolution proof system and we show that for every disjunctive FFO logic a refutationally complete resolution proof system can be constructed. Moreover, we discuss two theorem proving strategies, the polarity and set of support strategies, and we prove their completeness. © 1992, Academic Press Limited. All rights reserved.

Type: Article
Title: A resolution framework for finitely-valued first-order logics
DOI: 10.1016/S0747-7171(10)80002-1
UCL classification: UCL > Provost and Vice Provost Offices
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: http://discovery.ucl.ac.uk/id/eprint/1342374
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item