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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
