Proposition algebra
Authors:
Open Access
- 16 May 2011
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computational Logic
- Vol. 12 (3) , 1-36
Abstract
Sequential propositional logic deviates from conventional propositional logic by taking into account that during the sequential evaluation of a propositional statement, atomic propositions may yield different Boolean values at repeated occurrences. We introduce “free valuations” to capture this dynamics of a propositional statement's environment. The resulting logic is phrased as an equationally specified algebra rather than in the form of proof rules, and is named “proposition algebra.” It is strictly more general than Boolean algebra to the extent that the classical connectives fail to be expressively complete in the sequential case. The four axioms for free valuation congruence are then combined with other axioms in order define a few more valuation congruences that gradually identify more propositional statements, up to static valuation congruence (which is the setting of conventional propositional logic). Proposition algebra is developed in a fashion similar to the process algebra ACP and the program algebra PGA, via an algebraic specification which has a meaningful initial algebra for which a range of coarser congruences are considered important as well. In addition, infinite objects (i.e., propositional statements, processes and programs respectively) are dealt with by means of an inverse limit construction which allows the transfer of knowledge concerning finite objects to facts about infinite ones while reducing all facts about infinite objects to an infinity of facts about finite ones in return.Keywords
All Related Versions
This publication has 20 references indexed in Scilit:
- Thread algebra for strategic interleavingFormal Aspects of Computing, 2007
- Execution architectures for program algebraJournal of Applied Logic, 2007
- A Bypass of Cohen’s Impossibility ResultLecture Notes in Computer Science, 2005
- Reply to 'Comment on "A Framework for Modelling Trojans and Computer Virus Infection"' by E. MakinenThe Computer Journal, 2001
- Bochvar-McCarthy Logic and Process AlgebraNotre Dame Journal of Formal Logic, 1998
- Kleene's three-valued logic and process algebraInformation Processing Letters, 1998
- A propositional logic with 4 values: true, false, divergent and meaninglessJournal of Applied Non-Classical Logics, 1995
- Computer virusesComputers & Security, 1987
- Process algebra for synchronous communicationInformation and Control, 1984
- Varieties of ”If-Then-Else“SIAM Journal on Computing, 1983