Standard completeness of Hájek basic logic and decompositions of BL-chains

The aim of this paper is to survey the tools needed to prove the standard completeness of Hájek Basic Logic with respect to continuous t-norms. In particular, decompositions of totally ordered BL-algebras into simpler components are considered in some detail.     

Pseudo-t-norms and pseudo-BL algebras

BL algebras were introduced by Hájek as algebraic structures for his Basic Logic, starting from continuous t-norms on [0,1]. MV algebras, product algebras and Gödel algebras are particular cases of BL algebras. On the other hand, the pseudo-MV algebras extend the MV-algebras in the same way in which the arbitrary l-groups extend the abelian l-groups. We have generalized the BL algebras and pseudo-MV algebras, introducing the pseudo-BL algebras. In this paper we introduce weak-BL algebras and weak-pseudo-BL algebras. We also introduce non-commutative t-norms (we call them pseudo-t-norms) and use them in constructing pseudo-BL algebras and weak-pseudo-BL algebras.     

Alternative Proof of Standard Completeness Theorem for MTL

As it was shown in Jenei and Montagna (Studia Logica 70(2): 183–192, 2002), Monoidal t-norm based logic (MTL) is a logic of left-continuous t-norms. In other words, this means that MTL enjoys the standard completeness theorem. In this paper we present a different proof of this theorem. In fact, we prove even more since we show that MTL is complete w.r.t. the class of standard MTL-algebras with finite congruence lattice or equivalently with finitely many Archimedean classes. We also show the connection between the congruence lattice of an MTL-chain and its Archimedean classes.The author was supported by the Program “Information Society” under project 1ET100300517.     

Basic fuzzy logic and BL-algebras

 The many-valued propositional logic BL (basic fuzzy logic) is investigated. It is known to be complete for tautologies over BL-algebras (particular residuated lattices). Each continuous t-norm on [0,1] determines a BL-algebra; such algebras are called t-algebras. Two additional axioms B1, B2 are found such that BL+(B1,B2) is complete for tautologies over t-algebras. It remains open whether B1, B2 are provable in BL.     

Completeness and Counter-Example Generations of a Basic Protocol Logic: (Extended Abstract)

We give an axiomatic system in first-order predicate logic with equality for proving security protocols correct. Our axioms and inference rules derive the basic inference rules, which are explicitly or implicitly used in the literature of protocol logics, hence we call our axiomatic system Basic Protocol Logic (or BPL, for short). We give a formal semantics for BPL, and show the completeness theorem such that for any given query (which represents a correctness property) the query is provable iff it is true for any model. Moreover, as a corollary of our completeness proof, the decidability of provability in BPL holds for any given query. In our formal semantics we consider a “trace” any kind of sequence of primitive actions, counter-models (which are generated from an unprovable query) cannot be immediately regarded as realizable traces (i.e., attacked processes on the protocol in question). However, with the aid of Comon-Treinen's algorithm for the intruder deduction problem, we can determine whether there exists a realizable trace among formal counter-models, if any, generated by the proof-search method (used in our completeness proof). We also demonstrate that our method is useful for both proof construction and flaw analysis by using a simple example.     

On combinations of propositional dynamic logic and doxastic modal logics

We prove completeness and decidability results for a family of combinations of propositional dynamic logic and unimodal doxastic logics in which the modalities may interact. The kind of interactions we consider include three forms of commuting axioms, namely, axioms similar to the axiom of perfect recall and the axiom of no learning from temporal logic, and a Church–Rosser axiom. We investigate the influence of the substitution rule on the properties of these logics and propose a new semantics for the test operator to avoid unwanted side effects caused by the interaction of the classic test operator with the extra interaction axioms. This paper is a revised and extended version of Schmidt and Tishkovsky (2003).     

逻辑系统L*和BL*的广义演绎定理的逆定理

利用形式推演方法，给出逻辑系统L*和BL*的广义演绎定理逆定理的证明，并利用系统BL*的完备性定理及广义演绎定理证明系统BL*的强可靠性定理。     

The completeness of functional logic

A new first-order logic, functional logic, was proposed recently by Staples, Robinson and Hazel. The logic provides a formal means of describing and reasoning about dependence on an implicit parameter, a prime motivation being the unification of the Hoare logic used to reason about procedural programs with the powerful and well established techniques of classical logic. Viewed more abstractly, independently of possible applications, functional logic may be described as a logic with primitives, axioms and inference rules appropriate for reasoning about the properties of mathematical functions. In this paper, the completeness of functional logic is proved; that is, it is shown that any term of a theory in the logic which is true in all models is a theorem.This work was done while the author was a visitor to the Key Centre for Software Technology, Department of Computer Science, The University of Queensland, Queensland 4072, Australia.     

Resolution theorem proving in reified modal logics

This paper is concerned with the application of the resolution theorem proving method to reified logics. The logical systems treated include the branching temporal logics and logics of belief based on K and its extensions. Two important problems concerning the application of the resolution rule to reified systems are identified. The first is the redundancy in the representation of truth functional relationships and the second is the axiomatic reasoning about modal structure. Both cause an unnecessary expansion in the search space. We present solutions to both problems which allow the axioms defining the reified logic to be eliminated from the database during theorem proving hence reducing the search space while retaining completeness. We describe three theorem proving methods which embody our solutions and support our analysis with empirical results.Much of the research reported in this paper was supported by DTI IED SERC grant No. GR/F 35968, and was carried out whilst Han Reichgelt was at the University of Nottingham.