Institutional Login
Welcome!
To use the personalized features of this site, please
log in
or
register
.
If you have forgotten your username or password, we can
help
.
My Menu
Marked Items
Alerts
Order History
Saved Items
All
Favorites
Content Types
All
Publications
Journals
Book Series
Books
Reference Works
Protocols
Subject Collections
Architecture and Design
Behavioral Science
Biomedical and Life Sciences
Business and Economics
Chemistry and Materials Science
Computer Science
Earth and Environmental Science
Engineering
Humanities, Social Sciences and Law
Mathematics and Statistics
Medicine
Physics and Astronomy
Professional and Applied Computing
中文(简体)
中文(繁體)
English
Deutsch
한국어
日本語
Français
Español
العربية
Русский
Book Chapter
Converting non-classical matrix proofs into sequent-style systems
Book Series
Lecture Notes in Computer Science
Publisher
Springer Berlin / Heidelberg
ISSN
0302-9743 (Print) 1611-3349 (Online)
Volume
Volume 1104/1996
Book
Automated Deduction — Cade-13
DOI
10.1007/3-540-61511-3
Copyright
1996
ISBN
978-3-540-61511-8
Category
Session 6A
DOI
10.1007/3-540-61511-3_104
Pages
418-432
Subject Collection
Computer Science
SpringerLink Date
Saturday, January 21, 2006
Add to marked items
Add to shopping cart
Add to saved items
Permissions & Reprints
Recommend this chapter
PDF (931.6 KB)
Free Preview
Session 6A
Converting non-classical matrix proofs into sequent-style systems
Stephan Schmitt
1
and Christoph Kreitz
1
(1)
FG Intellektik, FB Informatik, TH Darmstadt, Alexanderstr. 10, 64283 Darmstadt, Germany
Abstract
We present a uniform algorithm fot transforming matrix proofs in classical, constructive, and modal logics into sequent style proofs. Making use of a similarity between matrix methods and Fitting's
prefixed tableaus
we first develop a procedure for extracting a prefixed sequent proof from a given matrix proof. By considering the additional restrictions on the order of rule applications we then extend this procedure into an algorithm which generates a conventional sequent proof.
Our algorithm is based on unified representations of matrix characterizations for various logics as well as of prefixed and usual sequent calculi. The peculiarities of a logic are encoded by certain parameters which are summarized in tables to be consulted by the algorithm.
Fulltext Preview (Small,
Large
)
References secured to subscribers.
more options
Find
Query Builder
Close
|
Clear
Title (ti)
Summary (su)
Author (au)
ISSN (issn)
ISBN (isbn)
DOI (doi)
And
Or
Not
(
)
* (wildcard)
"" (exact)
Within all content
Within this book series
Within this book
Export this chapter
Export this chapter as
RIS
|
Text
Frequently asked questions
|
General information on journals and books
|
Send us your feedback
|
Impressum
|
Contact
© Springer.
Part of Springer Science+Business Media
Privacy, Disclaimer, Terms and Conditions, © Copyright Information
MetaPress Privacy Policy
Remote Address: 38.107.191.113 • Server: MPWEB26
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)