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.

Proof-Search in Natural Deduction Calculus for Classical Propositional Logic

FERRARI, MAURO;FIORENTINI, CAMILLO
2015

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.
24th International Conference, TABLEAUX 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings
978-3-319-24311-5
978-3-319-24312-2
Tableaux
Wroclaw, Poland
September 21-24, 2015
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/2024708
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 8
social impact