A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful systems resides in their responsiveness to extensibility of their reasoning capabilities, being designed over rule-based programming languages that allow the user to build her own `programs to construct proofs' - the so-called proof tactics.
The present contribution discusses the implementation of an algorithm that generates sound and complete tableau systems for a very inclusive class of sufficiently expressive finite-valued propositional logics, and then illustrates some of the challenges and difficulties related to the algorithmic formation of automated theorem proving tactics for such logics. The procedure on whose implementation we will report is based on a generalized notion of analyticity of proof systems that is intended to guarantee termination of the corresponding automated tactics on what concerns theoremhood in our targeted logics.
The use of logical systems for problem-solving may be as diverse as in proving theorems in mathematics or in figuring out how to meet up with a friend. In either case, the problem solving activity is captured by the search for an \emph{argument}, broadly conceived as a certificate for a solution to the problem. Crucially, for such a certificate to be a solution, it has be \emph{valid}, and what makes it valid is that they are well-constructed according to a notion of inference for the underlying logical system. We provide a general framework uniformly describing the use of logic as a mathemati…
The paper proposes a new type of negation in multi-valued logics, providing a different way to answer the following question: what does it mean that some object language formula does not have a given truth-value. Along the way, the paper provides a general definition of truth and falsity in an arbitrary many-valued logic.
From the viewpoint of provability, we compare some Gentzen-type hypersequent calculi for first-order infinite-valued Łukasiewicz logic and for first-order rational Pavelka logic with each other and with Hájek's Hilbert-type calculi for these logics. The key aspect of our comparison is a density elimination proof for one of the hypersequent calculi considered.
In this paper we consider the class of truth-functional many-valued logics with a finite set of truth-values. The main result of this paper is the development of a new \emph{binary} sequent calculi (each sequent is a pair of formulae) for many valued logic with a finite set of truth values, and of Kripke-like semantics for it that is both sound and complete. We did not use the logic entailment based on matrix with a strict subset of designated truth values, but a different new kind of semantics based on the generalization of the classic 2-valued truth-invariance entailment. In order to define …
We propose a new definition of the representation theorem for many-valued logics, with modal operators as well, and define the stronger relationship between algebraic models of a given logic and relational structures used to define the Kripke possible-world semantics for it. Such a new framework offers a new semantics for many-valued logics based on the truth-invariance entailment. Consequently, it is substantially different from current definitions based on a matrix with a designated subset of logic values, used for the satisfaction relation, often difficult to fix. In the case when the many-…
In this paper, we investigate the many-valued version of coalgebraic modal logic through predicate lifting approach. Coalgebras, understood as generic transition systems, can serve as semantic structures for various kinds of modal logics. A well-known result in coalgebraic modal logic is that its completeness can be determined at the one-step level. We generalize the result to the finitely many-valued case by using the canonical model construction method. We prove the result for coalgebraic modal logics based on three different many-valued algebraic structures, including the finitely-valued Łu…
We give the quantum subset construction of orthomodular lattice-valued finite automata, then we show the equivalence between orthomodular lattice-valued finite automata, orthomodular lattice-valued deterministic finite automata and orthomodular lattice-valued finite automata with empty string-moves. Based on these equivalences, we study the algebraic operations on orthomodular lattice-valued regular languages, then we establish Kleene theorem in the frame of quantum logic.
This paper is focused on the study of modal logics defined from valued Kripke frames, and particularly, on computability and expressibility questions of modal logics of transitive Kripke frames evaluated over certain residuated lattices. It is shown that a large family of those logics -- including the ones arising from the standard MV and Product algebras -- yields an undecidable consequence relation. Later on, the behaviour of transitive modal Lukasiewicz logic is compared with that of its non transitive counterpart, exhibiting some particulars concerning computability and equivalence with ot…
We investigate some finitely-valued generalizations of propositional dynamic logic with tests. We start by introducing the (n+1)-valued Kripke models and a corresponding language based on a modal extension of Łukasiewicz many-valued logic. We illustrate the definitions by providing a framework for an analysis of the Rényi - Ulam searching game with errors. Our main result is the axiomatization of the theory of the (n+1)-valued Kripke models. This result is obtained through filtration of the canonical model of the smallest (n+1)-valued propositional dynamic logic.
In the present paper we consider the simplest non-classical extension $GL4$ of the well-known propositional provability logic $GL$ together with the notion of expressibility of formulas in a logic proposed by A. V. Kuznetsov. Conditions for expressibility of constants in the 4-valued extension $L\mathfrak{B}_2$ of $GL$ are found out, which were first announced in a author's paper in 1996.
We address the problem of integrating information coming from different sources. The information consists of facts that a central server collects and tries to combine using (a) a set of logical rules, i.e. a logic program, and (b) a hypothesis representing the server's own estimates. In such a setting incomplete information from a source or contradictory information from different sources necessitate the use of many-valued logics in which programs can be evaluated and hypotheses can be tested. To carry out such activities we propose a formal framework based on bilattices such as Belnap's four-…
Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed, using an abstract interpretation based on 3-valued first-order logic. In that work, concrete stores are finite 2-valued logical structures, and the sets of stores that can possibly arise during execution are represented (conservatively) using a certain family of finite 3-valued logical structures. In this paper, we show how 3-valued structures that arise in shape analysis can be …
In this paper, we present an abstract framework of many-valued modal logic with the interpretation of atomic propositions and modal operators as predicate lifting over coalgebras for an endofunctor on the category of sets. It generalizes Pattinson's stratification method for colagebraic modal logic to the many-valued setting. In contrast to standard techniques of canonical model construction and filtration, this method employs an induction principle to prove the soundness, completeness, and finite model property of the logics. As a consequence, we can lift a restriction on the previous approac…
Dynamic logic is a powerful framework for reasoning about imperative programs. An extension with a concurrent operator [18] was introduced to formalise programs running in parallel. In other direction, other authors proposed a systematic method for generating multi-valued propositional dynamic logics to reason about weighted programs [14]. This paper presents the first step of combining these two frameworks to introduce uncertainty in concurrent computations. In the developed framework, a weight is assigned to each branch of the parallel execution, resulting in a (possible) asymmetric parallel…
Several notions of bisimulation relations for probabilistic non-deterministic transition systems have been considered in the literature. We consider a novel testing-based behavioral equivalence called upper-expectation bisimilarity and develop its theory using standard results from linear algebra and functional analysis. We show that, for a wide class of systems, our new notion coincides with Segala's convex bisimilarity. We develop logical characterizations in terms of expressive probabilistic modal mu-calculi and a novel real-valued modal logic. We prove that upper-expectation bisimilarity i…
Behavioural equivalences can be characterized via bisimulations, modal logics and spoiler-defender games. In this paper we review these three perspectives in a coalgebraic setting, which allows us to generalize from the particular branching type of a transition system. We are interested in qualitative notions (classical bisimulation) as well as quantitative notions (bisimulation metrics). Our first contribution is to introduce a spoiler-defender bisimulation game for coalgebras in the classical case. Second, we introduce such games for the metric case and furthermore define a real-valued modal…
We study a many-valued generalization of Propositional Dynamic Logic where formulas in states and accessibility relations between states of a Kripke model are evaluated in a finite FL-algebra. One natural interpretation of this framework is related to reasoning about costs of performing structured actions. We prove that PDL over any finite FL-algebra is decidable. We also establish a general completeness result for a class of PDLs based on commutative integral FL-algebras with canonical constants.
MV-algebras are an algebraic semantics for Lukasiewicz logic and MV-algebras generated by a finite chain are Heyting algebras where the Godel implication can be written in terms of De Morgan and Moisil's modal operators. In our work, a fragment of trivalent Lukasiewicz logic is studied. The propositional and first-order logic is presented. The maximal consistent theories are studied as Monteiro's maximal deductive systems of the Lindenbaum-Tarski algebra, in both cases. Consequently, the adequacy theorem with respect to the suitable algebraic structures is proven.
In this paper, we present an experiment of our randomized hints strategy of automated reasoning for yielding Axiom(5) from Axiom(1)(2)(3)(4) of Infinite-Valued Lukasiewicz Logic. In the experiment, we randomly generated a set of hints with size ranging from 30 to 60 for guiding hyper-resolution based search by the theorem prover OTTER. We have successfully found the most useful hints list (with 30 clauses) among 150 * 6 hints lists. Also, we discuss a curious non-linear increase of generated clauses in deducing Axiom(5) by applying our randomized hints strategy.
The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a mechanism for producing a classic-like description of them in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent semantics so obtained, uniform (classically-labeled) cut-free standard analytic tableaux with possibly branching invertible rules and paired with proof strategies designed to guarantee termination of…
This paper aims at providing a comprehensive solution to the archaic open problem: how to define semantics of three-valued modal logic with vivid intuitive picture, convincing philosophical justification as well as versatile practical usage. Based on an existing line of work concerned with investigating three-valued logic out of innovative angles of view, we adopt a detour approach to interpret three-valued logic from a four-valued perspective, which results in the invention of an universal and systematic methodology for developing, explaining as well as utilizing three-valued modal logic. We …
The motivation for this paper comes out of our experience with teaching natural deduction (ND) and with the way this formal system is implemented by the \textsc{Coq} proof assistant, namely by means of so-called tactics, which are heuristics that transform a goal formula into a sequence of subgoals whose provability implies that of the original formula. We aim at capturing some of these tactics into a system of ND for minimal logic. Our goal is twofold: formal and didactic. The former delivers a formal system with its underlying heuristics to build proofs, which in turn serves our latter purpo…
In this book, we consider various many-valued logics: standard, linear, hyperbolic, parabolic, non-Archimedean, p-adic, interval, neutrosophic, etc. We survey also results which show the tree different proof-theoretic frameworks for many-valued logics, e.g. frameworks of the following deductive calculi: Hilbert's style, sequent, and hypersequent. We present a general way that allows to construct systematically analytic calculi for a large family of non-Archimedean many-valued logics: hyperrational-valued, hyperreal-valued, and p-adic valued logics characterized by a special format of semantics…
We propose an approach to optimally synthesize quantum circuits from non-permutative quantum gates such as Controlled-Square-Root-of-Not (i.e. Controlled-V). Our approach reduces the synthesis problem to multiple-valued optimization and uses group theory. We devise a novel technique that transforms the quantum logic synthesis problem from a multi-valued constrained optimization problem to a group permutation problem. The transformation enables us to utilize group theory to exploit the properties of the synthesis problem. Assuming a cost of one for each two-qubit gate, we found all reversible c…
This paper treats logic programming with three kinds of negation: default, weak and strict negations. A 3-valued logic model theory is discussed for logic programs with three kinds of negation. The procedure is constructed for negations so that a soundness of the procedure is guaranteed in terms of 3-valued logic model theory.
We consider an example of four valued semantics partially inspired by quantum computations and negation-like operations occurred therein. In particular we consider a representation of so called square root of negation within this four valued semantics as an operation which acts like a cycling negation. We define two variants of logical matrices performing different orders over the set of truth values. Purely formal logical result of our study consists in axiomatizing the logics of defined matrices as the systems of binary consequence relation and proving correctness and completeness theorems f…
The semantics of logic programs was originally described in terms of two-valued logic. Soon, however, it was realised that three-valued logic had some natural advantages, as it provides distinct values not only for truth and falsehood, but also for "undefined". The three-valued semantics proposed by Fitting and by Kunen are closely related to what is computed by a logic program, the third truth value being associated with non-termination. A different three-valued semantics, proposed by Naish, shared much with those of Fitting and Kunen but incorporated allowances for programmer intent, the thi…
In this paper we develop a 2-valued reduction of many-valued logics, into 2-valued multi-modal logics. Such an approach is based on the contextualization of many-valued logics with the introduction of higher-order Herbrand interpretation types, where we explicitly introduce the coexistence of a set of algebraic truth values of original many-valued logic, transformed as parameters (or possible worlds), and the set of classic two logic values. This approach is close to the approach used in annotated logics, but offers the possibility of using the standard semantics based on Herbrand interpretati…
We introduce BPDL, a combination of propositional dynamic logic PDL with the basic four-valued modal logic BK studied by Odintsov and Wansing (`Modal logics with Belnapian truth values', J. Appl. Non-Class. Log. 20, 279--301 (2010)). We modify the standard arguments based on canonical models and filtration to suit the four-valued context and prove weak completeness and decidability of BPDL.
Closed classes of three-valued logic generated by periodic symmetric funtions that equal $1$ in tuples from $\{1,2\}^n$ and equal $0$ on the rest tuples are considered. Criteria for bases existence and finite bases existence for these classes is obtained.
The aim of illocutionary logic is to explain how context can affect the meaning of certain special kinds of performative utterances. Recall that performative utterances are understood as follows: a speaker performs the illocutionary act (e.g. act of assertion, of conjecture, of promise) with the illocutionary force (resp. assertion, conjecture, promise) named by an appropriate performative verb in the way of representing himself as performing that act. In the paper I proposed many-valued interpretation of illocutionary forces understood as modal operators. As a result, I built up a non-Archime…
Classically, two propositions are logically equivalent precisely when they are true under the same logical valuations. Also, two logical valuations are distinct if, and only if, there is a formula that is true according to one valuation, and false according to the other. By a real-valued logic we mean a many-valued logic in the sense of Petr Hájek that is complete with respect to a subalgebra of truth values of a BL-algebra given by a continuous triangular norm on [0, 1]. Abstracting the two foregoing properties from classical logic leads us to two principles that a real-valued logic may or ma…
Continuing to pursue a research direction that we already explored in connection with Gödel-Dummett logic and Ruspini partitions, we show here that Łukasiewicz logic is able to express the notion of pseudo-triangular basis of fuzzy sets, a mild weakening of the standard notion of triangular basis. En route to our main result we obtain an elementary, logic-independent characterisation of triangular bases of fuzzy sets.
Intuitionistic Propositional Logic is proved to be an infinitely many valued logic by Kurt Gödel (1932), and it is proved by Stanisław Jaśkowski (1936) to be a countably many valued logic. In this paper, we provide alternative proofs for these theorems by using models of Saul Kripke (1959). Gödel's proof gave rise to an intermediate propositional logic (between intuitionistic and classical), that is known nowadays as Gödel or the Gödel-Dummet Logic, and is studied by fuzzy logicians as well. We also provide some results on the inter-definablility of propositional connectives in this logic.
In this work we study the decidability of a class of global modal logics arising from Kripke frames evaluated over certain residuated lattices, known in the literature as modal many-valued logics. We exhibit a large family of these modal logics which are undecidable, in contrast with classical modal logic and propositional logics defined over the same classes of algebras. This family includes the global modal logics arising from Kripke frames evaluated over the standard Lukasiewicz and Product algebras. We later refine the previous result, and prove that global modal Lukasiewicz and Product lo…
We present a novel approach, which is based on multiple-valued logic (MVL), to the verification and analysis of digital hardware designs, which extends the common ternary or quaternary approaches for simulations. The simulations which are performed in the more informative MVL setting reveal details which are either invisible or harder to detect through binary or ternary simulations. In equivalence verification, detecting different behavior under MVL simulations may lead to the discovery of a genuine binary nonequivalence or to a qualitative gap between two designs. The value of a variable in a…
Real-valued logics underlie an increasing number of neuro-symbolic approaches, though typically their logical inference capabilities are characterized only qualitatively. We provide foundations for establishing the correctness and power of such systems. We give a sound and strongly complete axiomatization that can be parametrized to cover essentially every real-valued logic, including all the common fuzzy logics. Our class of sentences are very rich, and each describes a set of possible real values for a collection of formulas of the real-valued logic, including which combinations of real valu…
LP$^{\supset,\mathsf{F}}$ is a three-valued paraconsistent propositional logic which is essentially the same as J3. It has most properties that have been proposed as desirable properties of a reasonable paraconsistent propositional logic. However, it follows easily from already published results that there are exactly 8192 different three-valued paraconsistent propositional logics that have the properties concerned. In this paper, properties concerning the logical equivalence relation of a logic are used to distinguish LP$^{\supset,\mathsf{F}}$ from the others. As one of the bonuses of focussi…
Logical systems with classical negation and means for sentential or propositional self-reference involve, in some way, paradoxical statements such as the liar. However, the paradox disappears if one replaces classical by an appropriate non-classical negation such as a paraconsistent one (no paradox arises if the liar is both true and false). We consider a non-Fregean logic which is a revised and extended version (Lewitzka 2012) of Epsilon-T-Logic originally introduced by (Straeter 1992) as a logic with a total truth predicate and propositional quantifiers. Self-reference is achieved by means o…
