Computing Publications

Publications Home » A decidable CLDS for some proposi...

A decidable CLDS for some propositional resource logics

Krysia Broda

Book Chapter
Computational logic: logic programming and beyond: essays in honour of Robert A.Kowalski, Part II
Volume 2408
pp.135–159
2002
Springer
ISBN 3-5404-3960-9
Abstract

The compilation approach for Labelled Deductive Systems (CLDS) is

a general logical framework. Previously, it has been applied to various resource logics within natural deduction, tableaux and clausal systems, and in the latter case to yield a

decidable first order system for Intuitionistic Logic (IL). In this paper the same clausal approach is used to obtain a decidable theorem prover for the implication fragments of propositional substructural Linear Logic (LL) and Relevance Logic (RL).

The CLDS refutation method is based around a semantic approach using a

translation technique utilising first-order logic

together with a simple theorem prover for the translated theory

using techniques drawn from Model Generation

procedures. The resulting system is shown to correspond to a standard LL(RL)

presentation as given by appropriate Hilbert axiom systems and to be

decidable.

BibTEX file for the publication
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.