Propositional calculus

Summary

Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives. Propositions that contain no logical connectives are called atomic propositions. Unlike first-order logic, propositional logic does not deal with non-logical objects, predicates about them, or quantifiers. However, all the machinery of propositional logic is included in first-order logic and higher-order logics. In this sense, propositional logic is the foundation of first-order logic and higher-order logic. Explanation Logical connectives are found in natural languages. In English for example, some examples are "and" (conjunction), "or" (disjunction), "not" (negation) and "if

Official source

https://en.wikipedia.org/wiki/Propositional_calculus

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (12)

Related publications

Related people (1)

Related people

Related units (1)

Related units

Related concepts (85)

Related concepts

Related courses (19)

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics as diverse as mathematical reasoning, combinatorics, discrete structures & algorithmic thinking.

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a program part or a language. Students will learn how to apply these concepts in their reasoning.

Related courses

Related lectures (72)

Related lectures

A template for constructing Bayesian networks in forensic biology cases when considering activity level propositions

Alex Biedermann, Christophe Champod

The hierarchy of propositions has been accepted amongst the forensic science community for some time. It is also accepted that the higher up the hierarchy the propositions are, against which the scientist are competent to evaluate their results, the more directly useful the testimony will be to the court. Because each case represents a unique set of circumstances and findings, it is difficult to come up with a standard structure for evaluation. One common tool that assists in this task is Bayesian networks (BNs). There is much diversity in the way that BN can be constructed. In this work, we develop a template for BN construction that allows sufficient flexibility to address most cases, but enough commonality and structure that the flow of information in the BN is readily recognised at a glance. We provide seven steps that can be used to construct BNs within this structure and demonstrate how they can be applied, using a case example.

ELSEVIER IRELAND LTD2018

On Polynomial Algorithms for Normalizing Formulas

Mario Bucev, Simon Guilloud, Viktor Kuncak

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem for two subtheories of Boolean algebra, giving a sound procedure for propositional logical equivalence that is incomplete in general but complete with respect to a subset of Boolean algebra axioms. We first show a new algorithm to produce a normal form for expressions in the theory of ortholattices (OL) in time O(n^2). We also consider an algorithm, recently presented but never evaluated in practice, producing a normal form for a slightly weaker theory, orthocomplemented bisemilattices (OCBSL), in time O(n log(n)^2). For both algorithms, we present an implementation and show efficiency in two domains. First, we evaluate the algorithms on large propositional expressions, specifically combinatorial circuits from a benchmark suite, as well as on large random formulas. Second, we implement and evaluate the algorithms in the Stainless verifier, a tool for verifying the correctness of Scala programs. We used these algorithms as a basis for a new formula simplifier, which is applied before valid verification conditions are saved into a persistent cache. The results show that normalization substantially increases cache hit ratio in large benchmarks.

2022

The 2nd competition on counter measures to 2D face spoofing attacks

André Anjos, Shubham Bansal, Ivana Chingovska, Naser Damer, Tiago De Freitas Pereira, Dushyant Goyal, Shubham Gupta, Tarun Krishna, Sébastien Marcel

As a crucial security problem, anti-spoofing in biometrics, and particularly for the face modality, has achieved great progress in the recent years. Still, new threats arrive in form of better, more realistic and more sophisticated spoofing attacks. The objective of the 2nd Competition on Counter Measures to 2D Face Spoofing Attacks is to challenge researchers to create counter measures effectively detecting a variety of attacks. The submitted propositions are evaluated on the Replay-Attack database and the achieved results are presented in this paper.

2013