SOME OBSERVATIONS ON THE LOGICAL FOUNDATIONS OF INDUCTIVE THEOREM PROVING

被引：4

作者：

Hetzl, Stefan ^{[1
]}

Wong, Tin Lok ^{[2
]}

机构：

[1] Vienna Univ Technol, Inst Discrete Math & Geometry, Wiedner Hauptstr 8-10, AT-1040 Vienna, Austria

[2] Univ Vienna, Kurt Godel Res Ctr Math Log, Wahringer Str 25, AT-1090 Vienna, Austria

来源：

LOGICAL METHODS IN COMPUTER SCIENCE | 2017年 / 13卷 / 04期

基金：

奥地利科学基金会;

关键词：

inductive theorem proving; arithmetical theories; proof theory; CHECKING; MODEL;

D O I：

10.23638/LMCS-13(4:10)2017

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of finding induction axioms which are sufficient for proving a goal. Based on this model, we then analyze the following aspects: the choice of a proof shape, the choice of an induction rule and the language of the induction formula. In particular, using model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving.

引用

页数：26

共 50 条

[1] Logical errors on proving theorem
Sari, C. K.
Waluyo, M.
Ainur, C. M.
Darmaningsih, E. N.
[J]. 1ST INTERNATIONAL CONFERENCE OF EDUCATION ON SCIENCES, TECHNOLOGY, ENGINEERING, AND MATHEMATICS (ICE-STEM), 2018, 948
[2] Analogy in Inductive Theorem Proving
Erica Melis
Jon Whittle
[J]. Journal of Automated Reasoning, 1999, 22 : 117 - 147
[3] Analogy in inductive theorem proving
Melis, E
Whittle, J
[J]. JOURNAL OF AUTOMATED REASONING, 1999, 22 (02) : 117 - 147
[4] Focused Inductive Theorem Proving
Baelde, David
Miller, Dale
Snow, Zachary
[J]. AUTOMATED REASONING, 2010, 6173 : 278 - +
[5] Proving Termination by Dependency Pairs and Inductive Theorem Proving
Carsten Fuhs
Jürgen Giesl
Michael Parting
Peter Schneider-Kamp
Stephan Swiderski
[J]. Journal of Automated Reasoning, 2011, 47 : 133 - 160
[6] Proving Termination by Dependency Pairs and Inductive Theorem Proving
Fuhs, Carsten
Giesl, Juergen
Parting, Michael
Schneider-Kamp, Peter
Swiderski, Stephan
[J]. JOURNAL OF AUTOMATED REASONING, 2011, 47 (02) : 133 - 160
[7] Inductive theorem proving for design specifications
Padawitz, P
[J]. JOURNAL OF SYMBOLIC COMPUTATION, 1996, 21 (01) : 41 - 99
[8] Machine Learning for Inductive Theorem Proving
Jiang, Yaqing
Papapanagiotou, Petros
Fleuriot, Jacques
[J]. ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION (AISC 2018), 2018, 11110 : 87 - 103
[9] Resolution theorem proving: A logical point of view
Leitsch, A
[J]. LOGIC COLLOQUIM 01, PROCEEDINGS, 2005, 20 : 3 - 42
[10] Inductive theorem proving based on tree grammars
Eberhard, Sebastian
Hetzl, Stefan
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2015, 166 (06) : 665 - 700

← 1 2 3 4 5 →