Title
"Classical" Programming-with-Proofs in lambdaPASym: An Analysis of Non-confluence
Abstract
. SymPA is a natural deduction system for Peano Arithmeticthat was developed in order to provide a basis for the programmingwith-proofs paradigm in a classical logic setting. In the paper we analyzeone of its main features: non-confluence. After looking at which rules cancause non-confluence, we develop in the system a formal proof for a formulathat can be seen as a simple but meaningful program specification.The computational behaviour of the corresponding term will be analysedby...
Year
Venue
Keywords
1997
TACS
classical logic,natural deduction
Field
DocType
ISBN
Judgment,Discrete mathematics,Deduction theorem,Paraconsistent logic,Minimal logic,Sequent calculus,Mathematical proof,Classical logic,Rule of inference,Mathematics,Calculus
Conference
3-540-63388-X
Citations 
PageRank 
References 
3
0.43
3
Authors
3
Name
Order
Citations
PageRank
Franco Barbanera135735.14
Stefano Berardi237351.58
Massimo Schivalocchi330.43