A proof system for finite trees

Patrick Blackburn, Wilfried Meyer-Viol, Maarten De Rijke

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

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 EXPTIMEcompleteness of the satisfiability problem, and a discussion of issues related to complexity and theorem proving.
OriginalsprogEngelsk
TitelComputer Science Logic - 9th International Workshop, CSL 1995 Annual Conference of the EACSL, Selected Papers
RedaktørerHans Kleine Buning
Antal sider20
ForlagSpringer
Publikationsdato1996
Sider86-105
ISBN (Trykt)3540613773, 9783540613770
DOI
StatusUdgivet - 1996
Udgivet eksterntJa
Begivenhed9th International Workshop on Computer Science Logic, CSL 1995 held as Annual Conference of the European Association for Computer Science, EACSL 1995 - Paderborn, Tyskland
Varighed: 22 sep. 199529 sep. 1995

Konference

Konference9th International Workshop on Computer Science Logic, CSL 1995 held as Annual Conference of the European Association for Computer Science, EACSL 1995
LandTyskland
ByPaderborn
Periode22/09/199529/09/1995
SponsorEuropean Union, HCM Euroconference Program, University of Paderborn, Universitätsgesellschaft Paderborn
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind1092
ISSN0302-9743

Citer dette