MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Matthews, Seándblp
Editor(s):
McCune, Williamdblp
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
Conference URL::
Downloading URL:
Event Address*:
Townsville, Australia
Language:
English
Event Date*
(no longer used):
July, 13-17
Organization:
Association for Automated Reasoning
Event Start Date:
14 May 2024
Event End Date:
14 May 2024
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
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