The Library
A proof system for finite trees
Tools
UNSPECIFIED (1996) A proof system for finite trees. In: 9th International Workshop on Computer Science Logic (CSL 95) / Annual Conference of the EACSL, UNIV PADERBORN, PADERBORN, GERMANY, SEP 22-29, 1995. Published in: COMPUTER SCIENCE LOGIC, 1092 pp. 86-105. ISBN 3-540-61377-3. ISSN 0302-9743.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
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 | ||||
Official Date: | 1996 | ||||
Dates: |
|
||||
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 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |