UNSPECIFIED (1996) A proof system for finite trees. In: 9th International Workshop on Computer Science Logic (CSL 95) / Annual Conference of the EACSL, SEP 22-29, 1995, UNIV PADERBORN, PADERBORN, GERMANY.

Full text not available from this repository.

Abstract

In this paper we introduce a description language for finite trees. Although we briefly note some of its intended applications, the main goal of the paper is to provide it with a sound and complete proof system. We do so using standard axioms from modal provability logic and modal logics of programs, and prove completeness by extending techniques due to Van Benthem and Meyer-Viol (1994) and Blackburn and Meyer-Viol (1994). We conclude with a proof of the EXPTIME-completeness of the satisfiability problem, and a discussion of issues related to complexity and theorem proving.

Item Type:	Conference Item (UNSPECIFIED)
Subjects:	Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Series Name:	LECTURE NOTES IN COMPUTER SCIENCE
Journal or Publication Title:	COMPUTER SCIENCE LOGIC
Publisher:	SPRINGER-VERLAG BERLIN
ISBN:	3-540-61377-3
ISSN:	0302-9743
Editor:	Buning, HK
Date:	1996
Volume:	1092
Number of Pages:	20
Page Range:	pp. 86-105
Publication Status:	Published
Title of Event:	9th International Workshop on Computer Science Logic (CSL 95) / Annual Conference of the EACSL
Location of Event:	UNIV PADERBORN, PADERBORN, GERMANY
Date(s) of Event:	SEP 22-29, 1995
URI:	http://wrap.warwick.ac.uk/id/eprint/17765

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item