http://hdl.handle.net/11320/3585 Mon, 01 Jun 2026 13:05:53 GMT 2026-06-01T13:05:53Z http://hdl.handle.net/11320/3647 Tytuł: Weak Completeness Theorem for Propositional Linear Time Temporal Logic Autorzy: Giero, Mariusz Abstrakt: We prove weak (finite set of premises) completeness theorem for extended propositional linear time temporal logic with irreflexive version of until-operator. We base it on the proof of completeness for basic propositional linear time temporal logic given in [20] which roughly follows the idea of the Henkin-Hasenjaeger method for classical logic. We show that a temporal model exists for every formula which negation is not derivable (Satisfiability Theorem). The contrapositive of that theorem leads to derivability of every valid formula. We build a tree of consistent and complete PNPs which is used to construct the model. Opis: The author is the winner of the Mizar Prize for Young Researchers in 2012 for this article.; I would like to thank Prof. Dr. Stephan Merz for valuable hints which helped me to prove the theorem. I would particularly like to thank Dr. Artur Korniłowicz who patiently answered a lot of my questions regarding writing this article. I would like to thank Dr. Josef Urban for discussions and encouragement to write the article. I would like to thank Prof. Andrzej Trybulec, Dr. Adam Naumowicz, Dr. Grzegorz Bancerek and Karol Pak for their help in preparation of the article. Sun, 01 Jan 2012 00:00:00 GMT http://hdl.handle.net/11320/3647 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3649 Tytuł: Free Term Algebras Autorzy: Bancerek, Grzegorz Abstrakt: We interoduce a new characterization of algebras of normal forms of term rewriting systems [35] as algerbras of term free in itself (any function from free generators into the algebra generates endomorphism of the algebra). Introduced algebras are free in classes of algebras satisfying some sets of equalities. Their universes are subsets of all terms and the denotations of operation symbols are partially identical with the operations of construction of terms. These algebras are compiler algebras requiring some equalities of terms, e.g., associativity of addition. Sun, 01 Jan 2012 00:00:00 GMT http://hdl.handle.net/11320/3649 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3648 Tytuł: The Friendship Theorem Autorzy: Pąk, Karol Abstrakt: In this article we prove the friendship theorem according to the article [1], which states that if a group of people has the property that any pair of persons have exactly one common friend, then there is a universal friend, i.e. a person who is a friend of every other person in the group. Sun, 01 Jan 2012 00:00:00 GMT http://hdl.handle.net/11320/3648 2012-01-01T00:00:00Z http://hdl.handle.net/11320/3643 Tytuł: The Gödel Completeness Theorem for Uncountable Languages Autorzy: Schlöder, Julian J.; Koepke, Peter Opis: This article is part of the first author’s Bachelor thesis under the supervision of the second author. Sun, 01 Jan 2012 00:00:00 GMT http://hdl.handle.net/11320/3643 2012-01-01T00:00:00Z