Skip navigation
Skip navigation

Stratification in Logics of Definitions

Tiu, Alwen


Proof systems for logics with recursive definitions typically impose a strict syntactic stratification on the body of a definition to ensure cut elimination and consistency of the logics, i.e., by forbidding any negative occurrences of the predicate being defined. Often such a restriction is too strong, as there are cases where such negative occurrences do not lead to inconsistency. Several logical frameworks based on logics of definitions have been used to mechanise reasoning about properties...[Show more]

CollectionsANU Research Publications
Date published: 2012
Type: Journal article
Source: Lecture Notes in Computer Science (LNCS)
DOI: 10.1007/978-3-642-31365-3_43


File Description SizeFormat Image
01_Tiu_Stratification_in_Logics_of_2012.pdf272.74 kBAdobe PDF    Request a copy

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator