A tableau calculus for a logic with constructive negation and an implementation of the related decision procedure is presented. This logic is an extension of Nelson logic and it has been used in the framework of program verification and timing analysis of combinatorial circuits. The decision procedure is tailored to shrink the search space of proofs and it is proved correct by using a semantical technique. It has been implemented in C++ language.

Avellone, A., Fiorentini, C., Fiorino, G., Moscato, U. (2004). A space efficient implementation of a tableau calculus for a logic with a constructive negation. In Computer Science Logic 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings (pp.488-502). Springer Verlag [10.1007/978-3-540-30124-0_37].

A space efficient implementation of a tableau calculus for a logic with a constructive negation

AVELLONE, ALESSANDRO;FIORINO, GUIDO GIUSEPPE;MOSCATO, UGO EMANUELE
2004

Abstract

A tableau calculus for a logic with constructive negation and an implementation of the related decision procedure is presented. This logic is an extension of Nelson logic and it has been used in the framework of program verification and timing analysis of combinatorial circuits. The decision procedure is tailored to shrink the search space of proofs and it is proved correct by using a semantical technique. It has been implemented in C++ language.
paper
logic, ATP, contructivism
English
18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL - September 20-24, 2004
2004
Marcinkowski, J; Tarlecki, A
Computer Science Logic 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings
9783540230243
2004
3210 LNCS
488
502
http://www.springerlink.com/content/7hw6qteg79p3he1t/fulltext.pdf
none
Avellone, A., Fiorentini, C., Fiorino, G., Moscato, U. (2004). A space efficient implementation of a tableau calculus for a logic with a constructive negation. In Computer Science Logic 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings (pp.488-502). Springer Verlag [10.1007/978-3-540-30124-0_37].
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/10281/1095
Citazioni
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 4
Social impact