Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
On sets, types, fixed points, and checkerboards Read chapter Read first chapter

1996 | ReviewPaper | Chapter

Strong normalization for all-style LKtq

Extended abstract

Authors : Jean-Baptiste Joinet, Harold Schellinx, Lorenzo Tortora de Falco

Published in: Theorem Proving with Analytic Tableaux and Related Methods

Publisher: Springer Berlin Heidelberg

Included in: Professional Book Archive

Get Access

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

We prove strong normalization of tq-reduction for all standard versions of sequent calculus for classical and intuitionistic (second and first order) logic and give a perspicuous argument for the completeness of the focusing restriction on sequent derivations.

previous chapter Efficient loop-check for backward proof search in some non-classical propositional logics
next chapter T-string unification: Unifying prefixes in non-classical proof methods
Metadata
Title
Strong normalization for all-style LKtq
Authors
Jean-Baptiste Joinet
Harold Schellinx
Lorenzo Tortora de Falco
Copyright Year
1996
Publisher
Springer Berlin Heidelberg
Book
Theorem Proving with Analytic Tableaux and Related Methods

Print ISBN: 978-3-540-61208-7

Electronic ISBN: 978-3-540-68368-1

Copyright Year: 1996

DOI
https://doi.org/10.1007/3-540-61208-4_15