Paper Info
Title
Proof-Search in Natural Deduction Calculus for Classical Propositional Logic.
Abstract
We address the problem of proof-search in the natural deduction calculus for Classical propositional logic. Our aim is to improve the usual naïve proof-search procedure where introduction rules are applied upwards and elimination rules downwards. In particular, we introduce NCR, a variant of the usual natural deduction calculus for Classical propositional logic, and we show that it can be used as a base for a proof-search procedure which does not require backtracking nor loop-checking.
Year
DOI
Venue
2015
10.1007/978-3-319-24312-2_17
TABLEAUX
Field
DocType
Volume
Discrete mathematics,Natural deduction,Computer science,Sequent calculus,Propositional calculus,Zeroth-order logic,Algorithm,Well-formed formula,Rule of inference,Calculus,Propositional variable,Curry–Howard correspondence
Conference
9323
ISSN
Citations 
PageRank 
0302-9743
3
0.47
References 
Authors
8
2
Name
Order
Citations
PageRank
Mauro Ferrari19316.05
Camillo Fiorentini212121.00