Publications: Journal Article: Automated Proof Construction in Type Theory using Resolution

Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

Options:

Goto entry point

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

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

Attachment Section