Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Matthews, Seán

dblp



Editor(s):

McCune, William

dblp



BibTeX cite key*:

Matthews97a

Title, Booktitle

Title*:

A practical implementation of simple consequence relations using inductive definitions

Booktitle*:

Proceedings of the 14th International Conference on Automated Deduction (CADE-14)

Event, URLs

URL of the conference:


URL for downloading the paper:


Event Address*:

Townsville, Australia

Language:

English

Event Date*
(no longer used):

July, 13-17

Organization:

Association for Automated Reasoning

Event Start Date:

19 July 2019

Event End Date:

19 July 2019

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

1249

Number:


Month:

July

Pages:

306-320

Year*:

1997

VG Wort Pages:


ISBN/ISSN:

3-540-63104-6

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) 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.

Keywords:

Logical frameworks, Inductive definitions, Interactive proof systems



Download
Access Level:


Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

experts only

Appearance:

MPG publications list, university publications list, working group publication list, Fachbeirat



BibTeX Entry:

@INPROCEEDINGS{Matthews97a,
AUTHOR = {Matthews, Se{\'a}n},
EDITOR = {McCune, William},
TITLE = {A practical implementation of simple consequence relations using inductive definitions},
BOOKTITLE = {Proceedings of the 14th International Conference on Automated Deduction (CADE-14)},
PUBLISHER = {Springer},
YEAR = {1997},
ORGANIZATION = {Association for Automated Reasoning},
VOLUME = {1249},
PAGES = {306--320},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Townsville, Australia},
MONTH = {July},
ISBN = {3-540-63104-6},
}


Entry last modified by Uwe Brahm, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Seán Matthews
Created
04/22/1997 10:52:48 AM
Revisions
8.
7.
6.
5.
4.
Editor(s)
Uwe Brahm
Uwe Brahm
Uwe Brahm
Seán Matthews
Seán Matthews
Edit Dates
02/26/98 03:11:35 PM
02/25/98 06:56:36 PM
28.01.98 15:41:56
21/01/98 13:02:05
21/01/98 12:29:30