A Practical Implementation of Simple Consequence Relations Using Inductive 
Definitions

Matthews, Seán

doi:10.1007/3-540-63104-6_31

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

A Practical Implementation of Simple Consequence Relations Using Inductive Definitions

MPS-Authors

/persons/resource/persons45002

Matthews, Seán
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

https://rdcu.be/dwqqC
(Publisher version)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Matthews, S. (1997). A Practical Implementation of Simple Consequence Relations Using Inductive Definitions. In W. McCune (Ed.), Automated Deduction - CADE-14 (pp. 306-320). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-39D0-9

Abstract

Logical frameworks such as the Edinburgh LF or Isabelle are not
suitable for general metatheory, since they do not allow induction.
On the other hand it is hard to encode a logic in an inductive
definition-style framework so that it is usable for object theory. We
propose a solution to this problem that borrows techniques from the
type-theory tradition of logical frameworks for use with a language of
inductive definitions, providing us with a notation suitable for
practical object and metatheory both.