Cultural advice

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

Aboriginal and Torres Strait Islander peoples are advised that ANU Library collections may include images, names, voices, and other representations of deceased persons.

Material in the collection may contain terms, language or views that reflect the period in which the item was created and may be considered inappropriate today.

A logic for reasoning about generic judgments

Date

Authors

Tiu, Alwen

Publisher

Elsevier

Abstract

This paper presents an extension of a proof system for encoding generic judgments, the logic FOλΔ ∇ of Miller and Tiu, with an induction principle. The logic FOλΔ ∇ is itself an extension of intuitionistic logic with fixed points and a "generic qu

Keywords

Case based reasoning, Encoding (symbols), Problem solving, Specifications, Generic Judgments, Higher-order abstract syntax, Logical frameworks, Proof theory, Formal logic higher-order abstract syntax, logical frameworks, Proof theory

URI

http://hdl.handle.net/1885/39353

Collections

ANU Research Publications

Source

Electronic Notes in Theoretical Computer Science

Type

Journal article

DOI

10.1016/j.entcs.2007.01.016

Restricted until

2037-12-31

Downloads

File

Description

01_Tiu_A_logic_for_reasoning_about_2007.pdf (457.01 KB)