Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic

被引：3

作者：

Ferrari, Mauro ^{[1
]}

Fiorentini, Camillo ^{[2
]}

机构：

[1] Univ Insubria, Dipartimento Sci Teor & Applicate, Via Mazzini 5, I-21100 Varese, Italy

[2] Univ Milan, Dipartimento Informat, Via Comelico 39, I-20135 Milan, Italy

来源：

JOURNAL OF AUTOMATED REASONING | 2019年 / 62卷 / 01期

关键词：

Natural deduction; Intuitionistic propositional logic; Proof-search procedures; CALCULUS; SEQUENT;

D O I：

10.1007/s10817-017-9427-3

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We address the problem of proof-search in the natural deduction calculus for Intuitionistic propositional logic. Our aim is to improve the usual proof-search procedure where introduction rules are applied upwards and elimination rules downwards. In particular, we introduce Nbu, a variant of the usual natural deduction calculus for Intuitionistic Propositional Logic, and we show that it can be used as a base for a goal-oriented proof-search procedure. We also show that the implementation of our proof-search procedure is competitive with those based on sequent or tableaux calculi.

引用

页码：127 / 167

页数：41

共 50 条

[1] Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic
Mauro Ferrari
Camillo Fiorentini
Journal of Automated Reasoning, 2019, 62 : 127 - 167
[2] Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
Ferrari, Mauro
Fiorentini, Camillo
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2015), 2015, 9323 : 237 - 252
[3] A proof-search procedure for intuitionistic propositional logic
R. Alonderis
Archive for Mathematical Logic, 2013, 52 : 759 - 778
[4] A proof-search procedure for intuitionistic propositional logic
Alonderis, R.
ARCHIVE FOR MATHEMATICAL LOGIC, 2013, 52 (7-8) : 759 - 778
[5] ADC method of proof search for intuitionistic propositional natural deduction
Mints, G.
Steinert-Threlkeld, Sh.
JOURNAL OF LOGIC AND COMPUTATION, 2016, 26 (01) : 395 - 408
[6] Proof-search in intuitionistic logic based on constraint satisfaction
Voronkov, A
THEOREM PROVING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1996, 1071 : 312 - 329
[7] Proof-search, analytic tableaux, models and counter-models, in Hypo constructive semantics for Minimal and Intuitionistic Propositional Logic
Sanz, Wagner
Journal of Applied Logics, 2022, 9 (01): : 541 - 572
[8] PROOF-SEARCH, ANALYTIC TABLEAUX, MODELS AND COUNTER-MODELS, IN HYPO CONSTRUCTIVE SEMANTICS FOR MINIMAL AND INTUITIONISTIC PROPOSITIONAL LOGIC
Sanz, Wagner
JOURNAL OF APPLIED LOGICS-IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS, 2022, 9 (01): : 541 - 571
[9] Efficient SAT-based Proof Search in Intuitionistic Propositional Logic
Fiorentini, Camillo
AUTOMATED DEDUCTION, CADE 28, 2021, 12699 : 217 - 233
[10] A proof-search system for the logic of likelihood
Alonderis, R.
Giedra, H.
LOGIC JOURNAL OF THE IGPL, 2020, 28 (03) : 261 - 280

← 1 2 3 4 5 →