W BIAŁYMSTOKU
Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/21372Pełny rekord metadanych
| Pole DC | Wartość | Język |
|---|---|---|
| dc.contributor.author | Braselmann, Patrick | - |
| dc.contributor.author | Koepke, Peter | - |
| dc.date.accessioned | 2026-10-29T12:27:06Z | - |
| dc.date.available | 2026-10-29T12:27:06Z | - |
| dc.date.issued | 2005 | - |
| dc.identifier.citation | Formalized Mathematics, Volume 13, Issue 1, Pages 33-39 | pl |
| dc.identifier.issn | 1426-2630 | - |
| dc.identifier.uri | http://hdl.handle.net/11320/21372 | - |
| dc.description.abstract | This article is part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt Godel’s famous completeness theorem (K. Godel, “Die Vollstandigkeit der Axiome des logischen Funktionenkalkuls”, Monatshefte fur Mathematik und Physik 37 (1930), 349–360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article introduces a sequent calculus for first-order logic. The correctness of this calculus is shown and some important inferences are derived. The contents of this article correspond to Chapter IV of Ebbinghaus, Flum, Thomas. | pl |
| dc.language.iso | en | pl |
| dc.publisher | University of Białystok | pl |
| dc.rights | Attribution-ShareAlike 4.0 International | - |
| dc.rights.uri | https://creativecommons.org/licenses/by-sa/4.0/ | - |
| dc.title | A Sequent Calculus for First-Order Logic | pl |
| dc.type | Article | pl |
| dc.rights.holder | © 2005 University of Białystok | pl |
| dc.rights.holder | This work is licensed under the Creative Commons License. | pl |
| dc.description.Affiliation | Patrick Braselmann - University of Bonn | pl |
| dc.description.Affiliation | Peter Koepke - University of Bonn | pl |
| dc.description.references | Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. Sequences of ordinal numbers. Formalized Mathematics, 1(2):281–290, 1990. | pl |
| dc.description.references | Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finitesequences. Formalized Mathematics, 1(1):107–114, 1990. | pl |
| dc.description.references | Patrick Braselmann and Peter Koepke. Coincidence lemma and substitution lemma. Formalized Mathematics, 13(1):17–26, 2005. | pl |
| dc.description.references | Patrick Braselmann and Peter Koepke. Substitution in first-order formulas: Elementary properties. Formalized Mathematics, 13(1):5–15, 2005. | pl |
| dc.description.references | Patrick Braselmann and Peter Koepke. Substitution in first-order formulas. Part II. The construction of first-order formulas. Formalized Mathematics, 13(1):27–32, 2005. | pl |
| dc.description.references | Czesław Byliński. A classical first order language. Formalized Mathematics, 1(4):669–676, 1990. | pl |
| dc.description.references | Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990. | pl |
| dc.description.references | Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. | pl |
| dc.description.references | Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. | pl |
| dc.description.references | Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. | pl |
| dc.description.references | Agata Darmochwa l. A first–order predicate calculus. Formalized Mathematics, 1(4):689–695, 1990. | pl |
| dc.description.references | Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303–311, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics. | pl |
| dc.description.references | Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Function domains and Frænkel operator. Formalized Mathematics, 1(3):495–500, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990. | pl |
| dc.description.references | Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Interpretation and satisfiability in the first order logic. Formalized Mathematics, 1(4):739–743, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Many–argument relations. Formalized Mathematics, 1(4):733–737, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990. | pl |
| dc.identifier.eissn | 1898-9934 | - |
| dc.description.volume | 13 | pl |
| dc.description.issue | 1 | pl |
| dc.description.firstpage | 33 | pl |
| dc.description.lastpage | 39 | pl |
| dc.identifier.citation2 | Formalized Mathematics | pl |
| Występuje w kolekcji(ach): | Formalized Mathematics, 2005, Volume 13, Issue 1 | |
Pliki w tej pozycji:
| Plik | Opis | Rozmiar | Format | |
|---|---|---|---|---|
| A_Sequent_Calculus_for_First_Order_Logic.pdf | 105,67 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL
