Propositional calculus

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. Logical connectives are found in natural languages. In English for example, some examples are "and" (conjunction), "or" (disjunction), "not" (negation) and "if" (but only when used to denote material conditional). The following is an example of a very simple inference within the scope of propositional logic: Premise 1: If it's raining then it's cloudy. Premise 2: It's raining. Conclusion: It's cloudy. Both premises and the conclusion are propositions. The premises are taken for granted, and with the application of modus ponens (an inference rule), the conclusion follows. As propositional logic is not concerned with the structure of propositions beyond the point where they can't be decomposed any more by logical connectives, this inference can be restated replacing those atomic statements with statement letters, which are interpreted as variables representing statements: Premise 1: Premise 2: Conclusion: The same can be stated succinctly in the following way: When P is interpreted as "It's raining" and Q as "it's cloudy" the above symbolic expressions can be seen to correspond exactly with the original expression in natural language. Not only that, but they will also correspond with any other inference of this form, which will be valid on the same basis this inference is.

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 (3)

Related people (1)

Related units (1)

Related concepts (194)

Related courses (39)

Related lectures (416)

Related MOOCs (3)

, ,

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 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

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

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

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

Parallel programming

With every smartphone and computer now boasting multiple processors, the use of functional ideas to facilitate parallel programming is becoming increasingly widespread. In this course, you'll learn th

Parallel programming

Logic

Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or logical truths. It studies how conclusions follow from premises due to the structure of arguments alone, independent of their topic and content. Informal logic is associated with informal fallacies, critical thinking, and argumentation theory. It examines arguments expressed in natural language while formal logic uses formal language.

Conditional proof

A conditional proof is a proof that takes the form of asserting a conditional, and proving that the antecedent of the conditional necessarily leads to the consequent. The assumed antecedent of a conditional proof is called the conditional proof assumption (CPA). Thus, the goal of a conditional proof is to demonstrate that if the CPA were true, then the desired conclusion necessarily follows. The validity of a conditional proof does not require that the CPA be true, only that if it were true it would lead to the consequent.

Conjunction introduction

Conjunction introduction (often abbreviated simply as conjunction and also called and introduction or adjunction) is a valid rule of inference of propositional logic. The rule makes it possible to introduce a conjunction into a logical proof. It is the inference that if the proposition is true, and the proposition is true, then the logical conjunction of the two propositions and is true. For example, if it is true that "it is raining", and it is true that "the cat is inside", then it is true that "it is raining and the cat is inside".

CS-101: Advanced information, computation, communication I

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 a

MATH-410: Riemann surfaces

This course is an introduction to the theory of Riemann surfaces. Riemann surfaces naturally appear is mathematics in many different ways: as a result of analytic continuation, as quotients of complex

CS-550: Formal verification

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 u

Explores predicate logic, focusing on quantifiers and normal forms, emphasizing the importance of finding witnesses and counterexamples.

Covers the basics of discrete mathematics, focusing on logic, structures, and algorithms for computer systems.

Covers Predicate Logic, focusing on Quantifiers, CNF, and DNF.