**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.

Concept# Proof calculus

Summary

In mathematical logic, a proof calculus or a proof system is built to prove statements.
A proof system includes the components:
Language: The set L of formulas admitted by the system, for example, propositional logic or first-order logic.
Rules of inference: List of rules that can be employed to prove theorems from axioms and theorems.
Axioms: Formulas in L assumed to be valid. All theorems are derived from axioms.
Usually a given proof calculus encompasses more than a single particular formal system, since many proof calculi are under-determined and can be used for radically different logics. For example, a paradigmatic case is the sequent calculus, which can be used to express the consequence relations of both intuitionistic logic and relevance logic. Thus, loosely speaking, a proof calculus is a template or design pattern, characterized by a certain style of formal inference, that may be specialized to produce specific formal systems, namely by specifying the actual inference rules for such a system. There is no consensus among logicians on how best to define the term.
The most widely known proof calculi are those classical calculi that are still in widespread use:
The class of Hilbert systems, of which the most famous example is the 1928 Hilbert–Ackermann system of first-order logic;
Gerhard Gentzen's calculus of natural deduction, which is the first formalism of structural proof theory, and which is the cornerstone of the formulae-as-types correspondence relating logic to functional programming;
Gentzen's sequent calculus, which is the most studied formalism of structural proof theory.
Many other proof calculi were, or might have been, seminal, but are not widely used today.
Aristotle's syllogistic calculus, presented in the Organon, readily admits formalisation. There is still some modern interest in syllogisms, carried out under the aegis of term logic.
Gottlob Frege's two-dimensional notation of the Begriffsschrift (1879) is usually regarded as introducing the modern concept of quantifier to logic.
C.S.

Official source

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 courses (32)

Related lectures (414)

Related publications (91)

Related people (23)

Related concepts (13)

Related MOOCs (15)

Ontological neighbourhood

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

COM-406: Foundations of Data Science

We discuss a set of topics that are important for the understanding of modern data science but that are typically not taught in an introductory ML course. In particular we discuss fundamental ideas an

MATH-432: Probability theory

The course is based on Durrett's text book
Probability: Theory and Examples.

It takes the measure theory approach to probability theory, wherein expectations are simply abstract integrals.

It takes the measure theory approach to probability theory, wherein expectations are simply abstract integrals.

Algebra (part 1)

Un MOOC francophone d'algèbre linéaire accessible à tous, enseigné de manière rigoureuse et ne nécessitant aucun prérequis.

Algebra (part 1)

Un MOOC francophone d'algèbre linéaire accessible à tous, enseigné de manière rigoureuse et ne nécessitant aucun prérequis.

Algebra (part 2)

Un MOOC francophone d'algèbre linéaire accessible à tous, enseigné de manière rigoureuse et ne nécessitant aucun prérequis.

Deep inference

Deep inference names a general idea in structural proof theory that breaks with the classical sequent calculus by generalising the notion of structure to permit inference to occur in contexts of high structural complexity. The term deep inference is generally reserved for proof calculi where the structural complexity is unbounded; in this article we will use non-shallow inference to refer to calculi that have structural complexity greater than the sequent calculus, but not unboundedly so, although this is not at present established terminology.

Sequent

In mathematical logic, a sequent is a very general kind of conditional assertion. A sequent may have any number m of condition formulas Ai (called "antecedents") and any number n of asserted formulas Bj (called "succedents" or "consequents"). A sequent is understood to mean that if all of the antecedent conditions are true, then at least one of the consequent formulas is true. This style of conditional assertion is almost always associated with the conceptual framework of sequent calculus.

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.

Harmonic Forms and Riemann Surfaces

Explores harmonic forms on Riemann surfaces, covering uniqueness of solutions and the Riemann bilinear identity.

Sobolev Spaces in Higher Dimensions

Explores Sobolev spaces in higher dimensions, discussing derivatives, properties, and challenges with continuity.

Harmonic Forms: Main Theorem

Explores harmonic forms on Riemann surfaces and the uniqueness of solutions to harmonic equations.

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-ord ...

2024```
We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having po ...
```

Mario Paolone, Willem Lambrichts

In this paper, we present a model for the analytical computation of the power flow sensitivity coefficients (SCs) for hybrid AC/DC networks. The SCs are defined as the partial derivates of the nodal voltages with respect to the active and reactive power in ...

2024