Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

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

Action:

login to update

Options:








Author, Editor(s)

Author(s):

Basin, David A.
Matthews, Seán

dblp
dblp



BibTeX cite key*:

BasinMatthews96a

Title

Title*:

Adding Metatheoretic facilities to First-order Theories

Journal

Journal Title*:

Journal of Logic and Computation

Journal's URL:


Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Oxford University Press

Publisher's URL:


Publisher's
Address:


ISSN:

0955-792X

Vol, No, pp, Date

Volume*:

6

Number:

6

Publishing Date:

1996

Pages*:

835-849

Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

Generic proof systems like Isabelle provide some limited
but useful metatheoretic facilities for declared logics;
in particular, users can prove simple derived rules
and also `solve' formulae that contain metavariables - a
technique useful for program synthesis. We show how an
arbitrary first-order theory can be conservatively extended
to provide similar facilities, without a supporting
metatheory, and examine what the limitations of this
approach are.

URL for the Abstract:


Categories,
Keywords:

automatic programming, formal logic, theorem proving, metatheoretic facilities, first-order theories, generic proof systems, Isabelle, declared logics, derived rules, formula solving, metavariables, program synthesis, conservative extension, computer-assisted proof, logical frameworks, second-order logic

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


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:

@ARTICLE{BasinMatthews96a,
AUTHOR = {Basin, David A. and Matthews, Se{\'a}n},
TITLE = {Adding Metatheoretic facilities to First-order Theories},
JOURNAL = {Journal of Logic and Computation},
PUBLISHER = {Oxford University Press},
YEAR = {1996},
NUMBER = {6},
VOLUME = {6},
PAGES = {835--849},
ISBN = {0955-792X},
}


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
03/11/1997 02:59:58 PM
Revisions
4.
3.
2.
1.
0.
Editor(s)
Uwe Brahm
Uwe Brahm
Uwe Brahm
Seán Matthews
Seán Matthews
Edit Dates
20.03.97 19:00:34
20.03.97 17:00:28
16/03/97 00:31:39
11/03/97 15:02:08
11/03/97 14:59:58