Abstract
Propositional logic is the basis for any study of logic. The sentences of propositional logic are built from a set of unstructured atomic propositions that are combined using a number of logical connectives. Logical connectives are Boolean operators whose names come from natural language, such as “not”, “and”, “or” and “implies”, and they are given a formal meaning that mimics its usage in natural language.
This chapter is devoted to the study of classical propositional logic. The chapter starts with a presentation of both the syntax and the semantics of propositional logic. In other words, we describe both the set of sentences of the language of propositional logic, and characterise the meaning of those sentences (i.e. which sentences are valid or not). The notion of proof derivation is then introduced as a syntactic characterisation of logical inference, and the interplay between provability and validity is established. The chapter concludes with a discussion of the decision problem of checking whether a propositional formula is valid or not.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
More rigorously, any problem inNP is reducible in polynomial-time to SAT.
- 2.
It is not uncommon to find in the literature slightly different definitions for CNF and DNF, for instance allowing for instance constants ⊥ and ⊤ to appear inside conjunctions/disjunctions, disallowing repetitions of literals, etc.
- 3.
Proofs by contradiction are not possible in the intuitionistic setting mentioned in Sect. 2.3.1. The rule (RAA) is absent from proof systems for intuitionistic logic.
- 4.
- 5.
References
Aczel, P.: Schematic consequence. In: Gabbay, D.M. (ed.) What Is a Logical System? Studies in Logic and Computation, pp. 261–272. Springer, Berlin (1994)
Goubault-Larrecq, J., Mackie, I.: Proof Theory and Automated Deduction. Applied Logic Series, vol. 6. Kluwer Academic, Dordrecht (1997)
Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)
Hoos, H.H., Stutzle, T.: Satlib: an online resource for research on sat. In: Walsh, T., Gent, I.P., v. Maaren, H. (eds.) SAT 2000, pp. 283–292. IOS Press, Amsterdam (2000)
Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in sat-based formal verification. Int. J. Softw. Tools Technol. Transf. (STTT)7(2), 156–173 (2005)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2011 Springer-Verlag London Limited
About this chapter
Cite this chapter
Almeida, J.B., Frade, M.J., Pinto, J.S., Melo de Sousa, S. (2011). Propositional Logic. In: Rigorous Software Development. Undergraduate Topics in Computer Science. Springer, London. https://doi.org/10.1007/978-0-85729-018-2_3
Download citation
DOI: https://doi.org/10.1007/978-0-85729-018-2_3
Publisher Name: Springer, London
Print ISBN: 978-0-85729-017-5
Online ISBN: 978-0-85729-018-2
eBook Packages: Computer ScienceComputer Science (R0)