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.
A space efficient implementation of a tableau calculus for a logic with a constructive negation / A. Avellone, C. Fiorentini, G. Fiorino, U. Moscato - In: Computer science logic : 18th International workshop, CSL 2004, 13th Annual Conference of the EACSL : Karpacz, Poland, september 20-24, 2004 : proceedings / [a cura di] J. Marcinkowski, A. Tarlecki. - Berlin : Springer, 2004. - ISBN 9783540230243. - pp. 488-502 (( Intervento presentato al 18. convegno International workshop on computer science logic tenutosi a Karpacz, Poland nel 2004 [10.1007/978-3-540-30124-0_37].
A space efficient implementation of a tableau calculus for a logic with a constructive negation
C. FiorentiniSecondo
;
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
2004_csl.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
Dimensione
239.09 kB
Formato
Adobe PDF
|
239.09 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
