Electronic Journal Article
@Article
Zeitschriftenartikel in einem e-Journal



Show entries of:

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

Action:

login to update

Options:




Library Locked Library locked




Author, Editor

Author(s):

Burel, Guillaume

dblp



BibTeX cite key*:

Burel2010a

Title

Title*:

Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo

Journal

Journal Title*:

Logical Methods in Computer Science

Journal's URL:

http://www.lmcs-online.org/

Download URL
for the article:

http://arxiv.org/pdf/0805.1464v4

Language:

English

Publisher

Publisher's
Name:

Department of Theoretical Computer Science, Technical University of Braunschweig

Publisher's URL:


Publisher's
Address:

Braunschweig

ISSN:

1860-5974

Vol, No, Year, pp.

Volume:

7

Number:

1

Month:


Year*:

2011

Pages:

3:1-3:31

Number of VG Pages:


Sequence Number:

3

DOI:

10.2168/LMCS-7 (1:3) 2011

Abstract, Links, (C)

Note:

Accepted, preparing publication

(LaTeX) Abstract:

In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for instance natural deduction---are applied. Therefore, the reasoning that is intrinsic of the theory does not appear in the length of proofs. In general, the congruence is defined through a rewrite system over terms and propositions. We define a rigorous framework to study proof lengths in deduction modulo, where the congruence must be computed in polynomial time. We show that even very simple rewrite systems lead to arbitrary proof-length speed-ups in deduction modulo, compared to using axioms. As higher-order logic can be encoded as a first-order theory in deduction modulo, we also study how to reinterpret, thanks to deduction modulo, the speed-ups between higher-order and first-order arithmetics that were stated by G\"odel. We define a first-order rewrite system with a congruence decidable in polynomial time such that proofs of higher-order arithmetic can be linearly translated into first-order arithmetic modulo that system. We also present the whole higher-order arithmetic as a first-order system without resorting to any axiom, where proofs have the same length as in the axiomatic presentation.

URL for the Abstract:

http://arxiv.org/abs/0805.1464

Categories / Keywords:

Proof Theory, Proof Complexity

HyperLinks / References / URLs:


Copyright Message:

Creative Commons

Personal Comments:


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Appearance:

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



BibTeX Entry:

@MISC{Burel2010a,
AUTHOR = {Burel, Guillaume},
TITLE = {Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo},
JOURNAL = {Logical Methods in Computer Science},
PUBLISHER = {Department of Theoretical Computer Science, Technical University of Braunschweig},
YEAR = {2011},
NUMBER = {1},
VOLUME = {7},
PAGES = {3:1--3:31},
ADDRESS = {Braunschweig},
ISBN = {1860-5974},
DOI = {10.2168/LMCS-7 (1:3) 2011},
NOTE = {Accepted, preparing publication},
}


Entry last modified by Anja Becker, 03/16/2012
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)
[Library]
Created
02/22/2011 10:02:53 AM
Revisions
4.
3.
2.
1.
0.
Editor(s)
Anja Becker
Anja Becker
Manuel Lamotte-Schubert
Anja Becker
Anja Becker
Edit Dates
16.03.2012 11:23:01
16.03.2012 11:22:41
16.03.2011 15:16:13
01.03.2011 14:31:44
02/22/2011 10:02:53 AM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section