Propositional calculus proving methods in Prolog
Propositional dynamic logic with recursive programs
Propositional Linear Temporal Logic with Initial Validity Semantics1
In the article [10] a formal system for Propositional Linear Temporal Logic (in short LTLB) with normal semantics is introduced. The language of this logic consists of “until” operator in a very strict version. The very strict “until” operator enables to express all other temporal operators. In this article we construct a formal system for LTLB with the initial semantics [12]. Initial semantics means that we define the validity of the formula in a model as satisfaction in the initial state of model...
Provability in arithmetic and a schema of Grzegorczyk
Pseudo -algebras and -monoids
It is shown that pseudo -algebras are categorically equivalent to certain bounded -monoids. Using this result, we obtain some properties of pseudo -algebras, in particular, we can characterize congruence kernels by means of normal filters. Further, we deal with representable pseudo -algebras and, in conclusion, we prove that they form a variety.
(Pure) logic out of probability.
Today, Logic and Probability are mostly seen as independent fields with a separate history and set of foundations. Against this dominating perception, only a very few people (Laplace, Boole, Peirce) have suspected there was some affinity or relation between them. The truth is they have a considerable common ground which underlies the historical foundation of both disciplines and, in this century, has prompted notable thinkers as Reichenbach [14], Carnap [2] [3] or Popper [12] [13] (and Gaifman [5],...
Putting together Lukasiewicz and product logics.
In this paper we investigate a propositional fuzzy logical system LΠ which contains the well-known Lukasiewicz, Product and Gödel fuzzy logics as sublogics. We define the corresponding algebraic structures, called LΠ-algebras and prove the following completeness result: a formula φ is provable in the LΠ logic iff it is a tautology for all linear LΠ-algebras. Moreover, linear LΠ-algebras are shown to be embeddable in linearly ordered abelian rings with a strong unit and cancellation law.
QL-implications versus D-implications
This paper deals with two kinds of fuzzy implications: QL and Dishkant implications. That is, those defined through the expressions and respectively, where is a t-norm, is a t-conorm and is a strong negation. Special attention is due to the relation between both kinds of implications. In the continuous case, the study of these implications is focused in some of their properties (mainly the contrapositive symmetry and the exchange principle). Finally, the case of non continuous t-norms...
Qualitative reasoning in Bayesian networks.
Some probabilistic inference rules which can be compared with the inference rules of preferential logic are given and it will be shown how they work in graphical models, allowing qualitative plausible reasoning in Bayesian networks.
Quasi-uniform Space
In this article, using mostly Pervin [9], Kunzi [6], [8], [7], Williams [11] and Bourbaki [3] works, we formalize in Mizar [2] the notions of quasiuniform space, semi-uniform space and locally uniform space. We define the topology induced by a quasi-uniform space. Finally we formalize from the sets of the form ((X Ω) × X) ∪ (X × Ω), the Csaszar-Pervin quasi-uniform space induced by a topological space.
Qu'est-ce la complétude structurale ?
Radical parallelism on projective lines and non-linear models of affine spaces.
Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
In this article, we formalize some basic facts of Z-module. In the first section, we discuss the rank of submodule of Z-module and its properties. Especially, we formally prove that the rank of any Z-module is equal to or more than that of its submodules, and vice versa, and that there exists a submodule with any given rank that satisfies the above condition. In the next section, we mention basic facts of linear transformations between two Z-modules. In this section, we define homomorphism between...
Reasoning in Basic Description Logics and Description Logics with Modal Operators
Reduced Products Of Saturated Intuitionistic Theories
Reduced products of saturated intuitionistic theories.
Reducibility method in simply typed lambda calculus.
Refined Morley numbers
Rekursive Unentscheidbarkeit der Theorie der pythagoräischen Körper
Relational specifications