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):

Bezem, Marc
Hendriks, Dimitri
de Nivelle, Hans

dblp
dblp
dblp

Not MPG Author(s):

Bezem, Marc
Hendriks, Dimitri

BibTeX cite key*:

deNivelle2002b

Title

Title*:

Automated Proof Construction in Type Theory using Resolution

Journal

Journal Title*:

Journal of Automated Reasoning

Journal's URL:

http://www.kluweronline.com/issn/0168-7433

Download URL
for the article:


Language:

English

Publisher

Publisher's
Name:

Kluwer

Publisher's URL:

http://www.wkap.nl

Publisher's
Address:

Dordrecht, the Netherlands

ISSN:

0168-7433

Vol, No, pp, Date

Volume*:

29

Number:

3/4

Publishing Date:

December 2002

Pages*:

253-275

Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) Abstract:

We provide techniques to integrate resolution logic with equality
in type theory. The results may be rendered as follows:
{\bf (1)}. A clausification procedure in type theory, equipped with
a correctness proof, all encoded using higher-order primitive recursion.
{\bf (2)}. A novel representation of clauses in minimal logic
such that the $ \lambda $-representation of resolution steps
is linear in the size of the premisses.
{\bf (3)}. Availability of the power of resolution theorem provers in interactive proof construction systems based on
type theory.

URL for the Abstract:


Categories,
Keywords:

type theory, proof construction, resolution theorem proving

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

Expert

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:

@ARTICLE{deNivelle2002b,
AUTHOR = {Bezem, Marc and Hendriks, Dimitri and de Nivelle, Hans},
TITLE = {Automated Proof Construction in Type Theory using Resolution},
JOURNAL = {Journal of Automated Reasoning},
PUBLISHER = {Kluwer},
YEAR = {2002},
NUMBER = {3/4},
VOLUME = {29},
PAGES = {253--275},
ADDRESS = {Dordrecht, the Netherlands},
MONTH = {December},
ISBN = {0168-7433},
}


Entry last modified by Christine Kiesel, 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)
Hans de Nivelle
Created
04/15/2003 01:46:13 PM
Revisions
3.
2.
1.
0.
Editor(s)
Christine Kiesel
Anja Becker
Hans de Nivelle
Hans de Nivelle
Edit Dates
01.09.2003 17:19:45
09.05.2003 10:05:39
04/15/2003 01:47:19 PM
04/15/2003 01:46:13 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section