Concepts of Proof in Mathematics, Philosophy, and Computer Science / / ed. by Dieter Probst, Peter Schuster.
A proof is a successful demonstration that a conclusion necessarily follows by logical reasoning from axioms which are considered evident for the given context and agreed upon by the community. It is this concept that sets mathematics apart from other disciplines and distinguishes it as the prototyp...
Saved in:
Superior document: | Title is part of eBook package: De Gruyter DG Plus DeG Package 2016 Part 1 |
---|---|
MitwirkendeR: | |
HerausgeberIn: | |
Place / Publishing House: | Berlin ;, Boston : : De Gruyter, , [2016] ©2016 |
Year of Publication: | 2016 |
Language: | English |
Series: | Ontos Mathematical Logic ,
6 |
Online Access: | |
Physical Description: | 1 online resource (X, 374 p.) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
9781501502620 |
---|---|
ctrlnum |
(DE-B1597)451552 (OCoLC)956701728 |
collection |
bib_alma |
record_format |
marc |
spelling |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / ed. by Dieter Probst, Peter Schuster. Berlin ; Boston : De Gruyter, [2016] ©2016 1 online resource (X, 374 p.) text txt rdacontent computer c rdamedia online resource cr rdacarrier text file PDF rda Ontos Mathematical Logic , 2198-2341 ; 6 Frontmatter -- Preface -- Contents -- Introduction -- Herbrand Confluence for First-Order Proofs with Π2-Cuts -- Proof-Oriented Categorical Semantics -- Logic for Gray-code Computation -- The Continuum Hypothesis Implies Excluded Middle -- Theories of Proof-Theoretic Strength Ψ (ΓΩ +1) -- Some Remarks about Normal Rings -- On Sets of Premises -- Non-Deterministic Inductive Definitions and Fullness -- Cyclic Proofs for Linear Temporal Logic -- Craig Interpolation via Hypersequents -- A General View on Normal Form Theorems for Łukasiewicz Logic with Product -- Relating Quotient Completions via Categorical Logic -- Some Historical, Philosophical and Methodological Remarks on Proof in Mathematics -- Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line Construction -- Hilbert’s Programme and Ordinal Analysis -- Aristotle’s Deductive Logic: a Proof-Theoretical Study -- Remarks on Barr’s Theorem: Proofs in Geometric Theories restricted access http://purl.org/coar/access_right/c_16ec online access with authorization star A proof is a successful demonstration that a conclusion necessarily follows by logical reasoning from axioms which are considered evident for the given context and agreed upon by the community. It is this concept that sets mathematics apart from other disciplines and distinguishes it as the prototype of a deductive science. Proofs thus are utterly relevant for research, teaching and communication in mathematics and of particular interest for the philosophy of mathematics. In computer science, moreover, proofs have proved to be a rich source for already certified algorithms. This book provides the reader with a collection of articles covering relevant current research topics circled around the concept 'proof'. It tries to give due consideration to the depth and breadth of the subject by discussing its philosophical and methodological aspects, addressing foundational issues induced by Hilbert's Programme and the benefits of the arising formal notions of proof, without neglecting reasoning in natural language proofs and applications in computer science such as program extraction. Issued also in print. Mode of access: Internet via World Wide Web. In English. Description based on online resource; title from PDF title page (publisher's Web site, viewed 28. Feb 2023) Logic, Symbolic and mathematical. Mathematics. Proof theory. Mathematische Logik. Philosophie der Mathematik. Theoretische Informatik. PHILOSOPHY / Epistemology. bisacsh Mathematical Logic. Philosophy of Mathematics. Theoretical Computer Science. Afshari, Bahareh, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Benini, Marco, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Berger, Ulrich, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Bridges, Douglas S., contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Buchholtz, Ulrik, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Coquand, Thierry, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Došen, Kosta, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Hetzl, Stefan, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Ishihara, Hajime, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Jäger, Gerhard, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Kokkinis, Ioannis, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Kuznets, Roman, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Lapenta, Serafina, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Leigh, Graham E., contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Leuştean, Ioana, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Lombardi, Henri, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Maietti, Maria Emilia, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Miyamoto, Kenji, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Murawski, Roman, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Negri, Sara, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Nemoto, Takako, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Plato, Jan von, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Pohlers, Wolfram, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Probst, Dieter, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Probst, Dieter, editor. edt http://id.loc.gov/vocabulary/relators/edt Rathjen, Michael, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Rosolini, Giuseppe, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Schuster, Peter, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Schuster, Peter, editor. edt http://id.loc.gov/vocabulary/relators/edt Schwichtenberg, Helmut, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Strahm, Thomas, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Studer, Thomas, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Tsuiki, Hideki, contributor. ctb https://id.loc.gov/vocabulary/relators/ctb Title is part of eBook package: De Gruyter DG Plus DeG Package 2016 Part 1 9783110762501 Title is part of eBook package: De Gruyter DG Plus eBook-Package 2016 9783110701005 Title is part of eBook package: De Gruyter EBOOK PACKAGE COMPLETE 2016 9783110485103 ZDB-23-DGG Title is part of eBook package: De Gruyter EBOOK PACKAGE Philosophy 2016 9783110485301 ZDB-23-DPH EPUB 9781501502644 print 9781501510809 https://doi.org/10.1515/9781501502620 https://www.degruyter.com/isbn/9781501502620 Cover https://www.degruyter.com/document/cover/isbn/9781501502620/original |
language |
English |
format |
eBook |
author2 |
Afshari, Bahareh, Afshari, Bahareh, Benini, Marco, Benini, Marco, Berger, Ulrich, Berger, Ulrich, Bridges, Douglas S., Bridges, Douglas S., Buchholtz, Ulrik, Buchholtz, Ulrik, Coquand, Thierry, Coquand, Thierry, Došen, Kosta, Došen, Kosta, Hetzl, Stefan, Hetzl, Stefan, Ishihara, Hajime, Ishihara, Hajime, Jäger, Gerhard, Jäger, Gerhard, Kokkinis, Ioannis, Kokkinis, Ioannis, Kuznets, Roman, Kuznets, Roman, Lapenta, Serafina, Lapenta, Serafina, Leigh, Graham E., Leigh, Graham E., Leuştean, Ioana, Leuştean, Ioana, Lombardi, Henri, Lombardi, Henri, Maietti, Maria Emilia, Maietti, Maria Emilia, Miyamoto, Kenji, Miyamoto, Kenji, Murawski, Roman, Murawski, Roman, Negri, Sara, Negri, Sara, Nemoto, Takako, Nemoto, Takako, Plato, Jan von, Plato, Jan von, Pohlers, Wolfram, Pohlers, Wolfram, Probst, Dieter, Probst, Dieter, Probst, Dieter, Probst, Dieter, Rathjen, Michael, Rathjen, Michael, Rosolini, Giuseppe, Rosolini, Giuseppe, Schuster, Peter, Schuster, Peter, Schuster, Peter, Schuster, Peter, Schwichtenberg, Helmut, Schwichtenberg, Helmut, Strahm, Thomas, Strahm, Thomas, Studer, Thomas, Studer, Thomas, Tsuiki, Hideki, Tsuiki, Hideki, |
author_facet |
Afshari, Bahareh, Afshari, Bahareh, Benini, Marco, Benini, Marco, Berger, Ulrich, Berger, Ulrich, Bridges, Douglas S., Bridges, Douglas S., Buchholtz, Ulrik, Buchholtz, Ulrik, Coquand, Thierry, Coquand, Thierry, Došen, Kosta, Došen, Kosta, Hetzl, Stefan, Hetzl, Stefan, Ishihara, Hajime, Ishihara, Hajime, Jäger, Gerhard, Jäger, Gerhard, Kokkinis, Ioannis, Kokkinis, Ioannis, Kuznets, Roman, Kuznets, Roman, Lapenta, Serafina, Lapenta, Serafina, Leigh, Graham E., Leigh, Graham E., Leuştean, Ioana, Leuştean, Ioana, Lombardi, Henri, Lombardi, Henri, Maietti, Maria Emilia, Maietti, Maria Emilia, Miyamoto, Kenji, Miyamoto, Kenji, Murawski, Roman, Murawski, Roman, Negri, Sara, Negri, Sara, Nemoto, Takako, Nemoto, Takako, Plato, Jan von, Plato, Jan von, Pohlers, Wolfram, Pohlers, Wolfram, Probst, Dieter, Probst, Dieter, Probst, Dieter, Probst, Dieter, Rathjen, Michael, Rathjen, Michael, Rosolini, Giuseppe, Rosolini, Giuseppe, Schuster, Peter, Schuster, Peter, Schuster, Peter, Schuster, Peter, Schwichtenberg, Helmut, Schwichtenberg, Helmut, Strahm, Thomas, Strahm, Thomas, Studer, Thomas, Studer, Thomas, Tsuiki, Hideki, Tsuiki, Hideki, |
author2_variant |
b a ba b a ba m b mb m b mb u b ub u b ub d s b ds dsb d s b ds dsb u b ub u b ub t c tc t c tc k d kd k d kd s h sh s h sh h i hi h i hi g j gj g j gj i k ik i k ik r k rk r k rk s l sl s l sl g e l ge gel g e l ge gel i l il i l il h l hl h l hl m e m me mem m e m me mem k m km k m km r m rm r m rm s n sn s n sn t n tn t n tn j v p jv jvp j v p jv jvp w p wp w p wp d p dp d p dp d p dp d p dp m r mr m r mr g r gr g r gr p s ps p s ps p s ps p s ps h s hs h s hs t s ts t s ts t s ts t s ts h t ht h t ht |
author2_role |
MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR HerausgeberIn HerausgeberIn MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR HerausgeberIn HerausgeberIn MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR MitwirkendeR |
author_sort |
Afshari, Bahareh, |
title |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / |
spellingShingle |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / Ontos Mathematical Logic , Frontmatter -- Preface -- Contents -- Introduction -- Herbrand Confluence for First-Order Proofs with Π2-Cuts -- Proof-Oriented Categorical Semantics -- Logic for Gray-code Computation -- The Continuum Hypothesis Implies Excluded Middle -- Theories of Proof-Theoretic Strength Ψ (ΓΩ +1) -- Some Remarks about Normal Rings -- On Sets of Premises -- Non-Deterministic Inductive Definitions and Fullness -- Cyclic Proofs for Linear Temporal Logic -- Craig Interpolation via Hypersequents -- A General View on Normal Form Theorems for Łukasiewicz Logic with Product -- Relating Quotient Completions via Categorical Logic -- Some Historical, Philosophical and Methodological Remarks on Proof in Mathematics -- Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line Construction -- Hilbert’s Programme and Ordinal Analysis -- Aristotle’s Deductive Logic: a Proof-Theoretical Study -- Remarks on Barr’s Theorem: Proofs in Geometric Theories |
title_full |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / ed. by Dieter Probst, Peter Schuster. |
title_fullStr |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / ed. by Dieter Probst, Peter Schuster. |
title_full_unstemmed |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / ed. by Dieter Probst, Peter Schuster. |
title_auth |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / |
title_alt |
Frontmatter -- Preface -- Contents -- Introduction -- Herbrand Confluence for First-Order Proofs with Π2-Cuts -- Proof-Oriented Categorical Semantics -- Logic for Gray-code Computation -- The Continuum Hypothesis Implies Excluded Middle -- Theories of Proof-Theoretic Strength Ψ (ΓΩ +1) -- Some Remarks about Normal Rings -- On Sets of Premises -- Non-Deterministic Inductive Definitions and Fullness -- Cyclic Proofs for Linear Temporal Logic -- Craig Interpolation via Hypersequents -- A General View on Normal Form Theorems for Łukasiewicz Logic with Product -- Relating Quotient Completions via Categorical Logic -- Some Historical, Philosophical and Methodological Remarks on Proof in Mathematics -- Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line Construction -- Hilbert’s Programme and Ordinal Analysis -- Aristotle’s Deductive Logic: a Proof-Theoretical Study -- Remarks on Barr’s Theorem: Proofs in Geometric Theories |
title_new |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / |
title_sort |
concepts of proof in mathematics, philosophy, and computer science / |
series |
Ontos Mathematical Logic , |
series2 |
Ontos Mathematical Logic , |
publisher |
De Gruyter, |
publishDate |
2016 |
physical |
1 online resource (X, 374 p.) Issued also in print. |
contents |
Frontmatter -- Preface -- Contents -- Introduction -- Herbrand Confluence for First-Order Proofs with Π2-Cuts -- Proof-Oriented Categorical Semantics -- Logic for Gray-code Computation -- The Continuum Hypothesis Implies Excluded Middle -- Theories of Proof-Theoretic Strength Ψ (ΓΩ +1) -- Some Remarks about Normal Rings -- On Sets of Premises -- Non-Deterministic Inductive Definitions and Fullness -- Cyclic Proofs for Linear Temporal Logic -- Craig Interpolation via Hypersequents -- A General View on Normal Form Theorems for Łukasiewicz Logic with Product -- Relating Quotient Completions via Categorical Logic -- Some Historical, Philosophical and Methodological Remarks on Proof in Mathematics -- Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line Construction -- Hilbert’s Programme and Ordinal Analysis -- Aristotle’s Deductive Logic: a Proof-Theoretical Study -- Remarks on Barr’s Theorem: Proofs in Geometric Theories |
isbn |
9781501502620 9783110762501 9783110701005 9783110485103 9783110485301 9781501502644 9781501510809 |
issn |
2198-2341 ; |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA9 |
callnumber-sort |
QA 19.54 C67 42016EB |
url |
https://doi.org/10.1515/9781501502620 https://www.degruyter.com/isbn/9781501502620 https://www.degruyter.com/document/cover/isbn/9781501502620/original |
illustrated |
Not Illustrated |
dewey-hundreds |
500 - Science |
dewey-tens |
510 - Mathematics |
dewey-ones |
511 - General principles of mathematics |
dewey-full |
511.3/6 |
dewey-sort |
3511.3 16 |
dewey-raw |
511.3/6 |
dewey-search |
511.3/6 |
doi_str_mv |
10.1515/9781501502620 |
oclc_num |
956701728 |
work_keys_str_mv |
AT afsharibahareh conceptsofproofinmathematicsphilosophyandcomputerscience AT beninimarco conceptsofproofinmathematicsphilosophyandcomputerscience AT bergerulrich conceptsofproofinmathematicsphilosophyandcomputerscience AT bridgesdouglass conceptsofproofinmathematicsphilosophyandcomputerscience AT buchholtzulrik conceptsofproofinmathematicsphilosophyandcomputerscience AT coquandthierry conceptsofproofinmathematicsphilosophyandcomputerscience AT dosenkosta conceptsofproofinmathematicsphilosophyandcomputerscience AT hetzlstefan conceptsofproofinmathematicsphilosophyandcomputerscience AT ishiharahajime conceptsofproofinmathematicsphilosophyandcomputerscience AT jagergerhard conceptsofproofinmathematicsphilosophyandcomputerscience AT kokkinisioannis conceptsofproofinmathematicsphilosophyandcomputerscience AT kuznetsroman conceptsofproofinmathematicsphilosophyandcomputerscience AT lapentaserafina conceptsofproofinmathematicsphilosophyandcomputerscience AT leighgrahame conceptsofproofinmathematicsphilosophyandcomputerscience AT leusteanioana conceptsofproofinmathematicsphilosophyandcomputerscience AT lombardihenri conceptsofproofinmathematicsphilosophyandcomputerscience AT maiettimariaemilia conceptsofproofinmathematicsphilosophyandcomputerscience AT miyamotokenji conceptsofproofinmathematicsphilosophyandcomputerscience AT murawskiroman conceptsofproofinmathematicsphilosophyandcomputerscience AT negrisara conceptsofproofinmathematicsphilosophyandcomputerscience AT nemototakako conceptsofproofinmathematicsphilosophyandcomputerscience AT platojanvon conceptsofproofinmathematicsphilosophyandcomputerscience AT pohlerswolfram conceptsofproofinmathematicsphilosophyandcomputerscience AT probstdieter conceptsofproofinmathematicsphilosophyandcomputerscience AT rathjenmichael conceptsofproofinmathematicsphilosophyandcomputerscience AT rosolinigiuseppe conceptsofproofinmathematicsphilosophyandcomputerscience AT schusterpeter conceptsofproofinmathematicsphilosophyandcomputerscience AT schwichtenberghelmut conceptsofproofinmathematicsphilosophyandcomputerscience AT strahmthomas conceptsofproofinmathematicsphilosophyandcomputerscience AT studerthomas conceptsofproofinmathematicsphilosophyandcomputerscience AT tsuikihideki conceptsofproofinmathematicsphilosophyandcomputerscience |
status_str |
n |
ids_txt_mv |
(DE-B1597)451552 (OCoLC)956701728 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Title is part of eBook package: De Gruyter DG Plus DeG Package 2016 Part 1 Title is part of eBook package: De Gruyter DG Plus eBook-Package 2016 Title is part of eBook package: De Gruyter EBOOK PACKAGE COMPLETE 2016 Title is part of eBook package: De Gruyter EBOOK PACKAGE Philosophy 2016 |
is_hierarchy_title |
Concepts of Proof in Mathematics, Philosophy, and Computer Science / |
container_title |
Title is part of eBook package: De Gruyter DG Plus DeG Package 2016 Part 1 |
author2_original_writing_str_mv |
noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField noLinkedField |
_version_ |
1806143889251237888 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>08693nam a22013335i 4500</leader><controlfield tag="001">9781501502620</controlfield><controlfield tag="003">DE-B1597</controlfield><controlfield tag="005">20230228123812.0</controlfield><controlfield tag="006">m|||||o||d||||||||</controlfield><controlfield tag="007">cr || ||||||||</controlfield><controlfield tag="008">230228t20162016gw fo d z eng d</controlfield><datafield tag="019" ind1=" " ind2=" "><subfield code="a">(OCoLC)1003975718</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9781501502620</subfield></datafield><datafield tag="024" ind1="7" ind2=" "><subfield code="a">10.1515/9781501502620</subfield><subfield code="2">doi</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(DE-B1597)451552</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)956701728</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">DE-B1597</subfield><subfield code="b">eng</subfield><subfield code="c">DE-B1597</subfield><subfield code="e">rda</subfield></datafield><datafield tag="041" ind1="0" ind2=" "><subfield code="a">eng</subfield></datafield><datafield tag="044" ind1=" " ind2=" "><subfield code="a">gw</subfield><subfield code="c">DE</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA9.54</subfield><subfield code="b">.C67 2016eb</subfield></datafield><datafield tag="072" ind1=" " ind2="7"><subfield code="a">PHI004000</subfield><subfield code="2">bisacsh</subfield></datafield><datafield tag="082" ind1="0" ind2="4"><subfield code="a">511.3/6</subfield><subfield code="2">23</subfield></datafield><datafield tag="245" ind1="0" ind2="0"><subfield code="a">Concepts of Proof in Mathematics, Philosophy, and Computer Science /</subfield><subfield code="c">ed. by Dieter Probst, Peter Schuster.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Berlin ;</subfield><subfield code="a">Boston : </subfield><subfield code="b">De Gruyter, </subfield><subfield code="c">[2016]</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2016</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (X, 374 p.)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="347" ind1=" " ind2=" "><subfield code="a">text file</subfield><subfield code="b">PDF</subfield><subfield code="2">rda</subfield></datafield><datafield tag="490" ind1="0" ind2=" "><subfield code="a">Ontos Mathematical Logic ,</subfield><subfield code="x">2198-2341 ;</subfield><subfield code="v">6</subfield></datafield><datafield tag="505" ind1="0" ind2="0"><subfield code="t">Frontmatter -- </subfield><subfield code="t">Preface -- </subfield><subfield code="t">Contents -- </subfield><subfield code="t">Introduction -- </subfield><subfield code="t">Herbrand Confluence for First-Order Proofs with Π2-Cuts -- </subfield><subfield code="t">Proof-Oriented Categorical Semantics -- </subfield><subfield code="t">Logic for Gray-code Computation -- </subfield><subfield code="t">The Continuum Hypothesis Implies Excluded Middle -- </subfield><subfield code="t">Theories of Proof-Theoretic Strength Ψ (ΓΩ +1) -- </subfield><subfield code="t">Some Remarks about Normal Rings -- </subfield><subfield code="t">On Sets of Premises -- </subfield><subfield code="t">Non-Deterministic Inductive Definitions and Fullness -- </subfield><subfield code="t">Cyclic Proofs for Linear Temporal Logic -- </subfield><subfield code="t">Craig Interpolation via Hypersequents -- </subfield><subfield code="t">A General View on Normal Form Theorems for Łukasiewicz Logic with Product -- </subfield><subfield code="t">Relating Quotient Completions via Categorical Logic -- </subfield><subfield code="t">Some Historical, Philosophical and Methodological Remarks on Proof in Mathematics -- </subfield><subfield code="t">Cut Elimination in Sequent Calculi with Implicit Contraction, with a Conjecture on the Origin of Gentzen’s Altitude Line Construction -- </subfield><subfield code="t">Hilbert’s Programme and Ordinal Analysis -- </subfield><subfield code="t">Aristotle’s Deductive Logic: a Proof-Theoretical Study -- </subfield><subfield code="t">Remarks on Barr’s Theorem: Proofs in Geometric Theories</subfield></datafield><datafield tag="506" ind1="0" ind2=" "><subfield code="a">restricted access</subfield><subfield code="u">http://purl.org/coar/access_right/c_16ec</subfield><subfield code="f">online access with authorization</subfield><subfield code="2">star</subfield></datafield><datafield tag="520" ind1=" " ind2=" "><subfield code="a">A proof is a successful demonstration that a conclusion necessarily follows by logical reasoning from axioms which are considered evident for the given context and agreed upon by the community. It is this concept that sets mathematics apart from other disciplines and distinguishes it as the prototype of a deductive science. Proofs thus are utterly relevant for research, teaching and communication in mathematics and of particular interest for the philosophy of mathematics. In computer science, moreover, proofs have proved to be a rich source for already certified algorithms. This book provides the reader with a collection of articles covering relevant current research topics circled around the concept 'proof'. It tries to give due consideration to the depth and breadth of the subject by discussing its philosophical and methodological aspects, addressing foundational issues induced by Hilbert's Programme and the benefits of the arising formal notions of proof, without neglecting reasoning in natural language proofs and applications in computer science such as program extraction.</subfield></datafield><datafield tag="530" ind1=" " ind2=" "><subfield code="a">Issued also in print.</subfield></datafield><datafield tag="538" ind1=" " ind2=" "><subfield code="a">Mode of access: Internet via World Wide Web.</subfield></datafield><datafield tag="546" ind1=" " ind2=" "><subfield code="a">In English.</subfield></datafield><datafield tag="588" ind1="0" ind2=" "><subfield code="a">Description based on online resource; title from PDF title page (publisher's Web site, viewed 28. Feb 2023)</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Logic, Symbolic and mathematical.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Mathematics.</subfield></datafield><datafield tag="650" ind1=" " ind2="0"><subfield code="a">Proof theory.</subfield></datafield><datafield tag="650" ind1=" " ind2="4"><subfield code="a">Mathematische Logik.</subfield></datafield><datafield tag="650" ind1=" " ind2="4"><subfield code="a">Philosophie der Mathematik.</subfield></datafield><datafield tag="650" ind1=" " ind2="4"><subfield code="a">Theoretische Informatik.</subfield></datafield><datafield tag="650" ind1=" " ind2="7"><subfield code="a">PHILOSOPHY / Epistemology.</subfield><subfield code="2">bisacsh</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Mathematical Logic.</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Philosophy of Mathematics.</subfield></datafield><datafield tag="653" ind1=" " ind2=" "><subfield code="a">Theoretical Computer Science.</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Afshari, Bahareh, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Benini, Marco, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Berger, Ulrich, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Bridges, Douglas S., </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Buchholtz, Ulrik, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Coquand, Thierry, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Došen, Kosta, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Hetzl, Stefan, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Ishihara, Hajime, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Jäger, Gerhard, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Kokkinis, Ioannis, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Kuznets, Roman, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Lapenta, Serafina, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Leigh, Graham E., </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Leuştean, Ioana, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Lombardi, Henri, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Maietti, Maria Emilia, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Miyamoto, Kenji, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Murawski, Roman, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Negri, Sara, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Nemoto, Takako, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Plato, Jan von, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Pohlers, Wolfram, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Probst, Dieter, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Probst, Dieter, </subfield><subfield code="e">editor.</subfield><subfield code="4">edt</subfield><subfield code="4">http://id.loc.gov/vocabulary/relators/edt</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Rathjen, Michael, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Rosolini, Giuseppe, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Schuster, Peter, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Schuster, Peter, </subfield><subfield code="e">editor.</subfield><subfield code="4">edt</subfield><subfield code="4">http://id.loc.gov/vocabulary/relators/edt</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Schwichtenberg, Helmut, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Strahm, Thomas, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Studer, Thomas, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">Tsuiki, Hideki, </subfield><subfield code="e">contributor.</subfield><subfield code="4">ctb</subfield><subfield code="4">https://id.loc.gov/vocabulary/relators/ctb</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">DG Plus DeG Package 2016 Part 1</subfield><subfield code="z">9783110762501</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">DG Plus eBook-Package 2016</subfield><subfield code="z">9783110701005</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">EBOOK PACKAGE COMPLETE 2016</subfield><subfield code="z">9783110485103</subfield><subfield code="o">ZDB-23-DGG</subfield></datafield><datafield tag="773" ind1="0" ind2="8"><subfield code="i">Title is part of eBook package:</subfield><subfield code="d">De Gruyter</subfield><subfield code="t">EBOOK PACKAGE Philosophy 2016</subfield><subfield code="z">9783110485301</subfield><subfield code="o">ZDB-23-DPH</subfield></datafield><datafield tag="776" ind1="0" ind2=" "><subfield code="c">EPUB</subfield><subfield code="z">9781501502644</subfield></datafield><datafield tag="776" ind1="0" ind2=" "><subfield code="c">print</subfield><subfield code="z">9781501510809</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://doi.org/10.1515/9781501502620</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://www.degruyter.com/isbn/9781501502620</subfield></datafield><datafield tag="856" ind1="4" ind2="2"><subfield code="3">Cover</subfield><subfield code="u">https://www.degruyter.com/document/cover/isbn/9781501502620/original</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">978-3-11-070100-5 DG Plus eBook-Package 2016</subfield><subfield code="b">2016</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">978-3-11-076250-1 DG Plus DeG Package 2016 Part 1</subfield><subfield code="b">2016</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_BACKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_CL_MTPY</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_CL_PLTLJSIS</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_DGALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EBACKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EBKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_ECL_MTPY</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_ECL_PLTLJSIS</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_EEBKALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_ESSHALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_ESTMALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_SSHALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">EBA_STMALL</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">GBV-deGruyter-alles</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA11SSHE</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA12STME</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA13ENGE</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA17SSHEE</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA18STMEE</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">PDA5EBK</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">ZDB-23-DGG</subfield><subfield code="b">2016</subfield></datafield><datafield tag="912" ind1=" " ind2=" "><subfield code="a">ZDB-23-DPH</subfield><subfield code="b">2016</subfield></datafield></record></collection> |