A proof system for finite trees
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.
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|
|Number of Pages:||20|
|Page Range:||pp. 86-105|
|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|
Actions (login required)