相关论文: Um modelo alg\'ebrico do quantificador da Ubiquida…
This article reformulates the theory of computable physical models, previously introduced by the author, as a branch of applied model theory in first-order logic. It provides a semantic approach to the philosophy of science that…
We develop a framework for epistemic logic that combines relevant modal logic with classical propositional logic. In our framework the agent is modeled as reasoning in accordance with a relevant modal logic while the propositional fragment…
In analogy with the classical theory of Eichler integrals for integral weight modular forms, Lawrence and Zagier considered examples of Eichler integrals of certain half-integral weight modular forms. These served as early prototypes of a…
Quantum computational logics represent a logical abstraction from the circuit-theory in quantum computation. In these logics formulas are supposed to denote pieces of quantum information (qubits, quregisters or mixtures of quregisters),…
The unification problem in a propositional logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. When a unifiable formula has minimal complete…
Quantum logic has been introduced by Birkhoff and von Neumann as an attempt to base the logical primitives, the propositions and the relations and operations among them, on quantum theoretical entities, and thus on the related empirical…
We present a Coq formalization of the Quantified Reflection Calculus with one modality, or $\mathsf{QRC}_1$. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The…
This paper argues for a modal view of probability. The syntax and semantics of one particularly strong probability logic are discussed and some examples of the use of the logic are provided. We show that it is both natural and useful to…
We propose a modal study of the notion of bisimulation. Our contribution is threefold. First, we extend the basic modal language with a new modality $\nbi$, whose intended meaning is universal quantification over all states that are…
We propose a new quantifier elimination algorithm for the theory of linear real arithmetic. This algorithm uses as subroutine satisfiability modulo this theory, a problem for which there are several implementations available. The quantifier…
We consider a quantified version of the (propositional) modal logic $\mathsf{BK}$, proposed earlier by S. P. Odintsov and H. Wansing; this version will be denoted by $\mathsf{QBK}$. Using the canonical model method, we prove the strong…
In this letter I stress the role of causal reversibility (time-symmetry), together with causality and locality, in the justification of the quantum formalism. Firstly, in the algebraic quantum formalism, I show that the assumption of…
The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal…
Computability logic is a formal theory of (interactive) computability in the same sense as classical logic is a formal theory of truth. This approach was initiated very recently in "Introduction to computability logic" (Annals of Pure and…
In this paper we consider Modal Team Logic, a generalization of Classical Modal Logic in which it is possible to describe dependence phenomena between data. We prove that most known fragment of Full Modal Team Logic allow the elimination of…
The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this…
Doubts are raised concerning the usual interpretation of the alleged failure, by quantum mechanics, of the distributive law of classical logic. The difficulty raised by incompatible sets of observables is overcome within an epistemic…
Our aim is to solve a quite old question on the difference between expandability and compact expandability. Toward this, we further investigate the logic of countable cofinality.
In a case study we investigate whether off the shelf higher-order theorem provers and model generators can be employed to automate reasoning in and about quantified multimodal logics. In our experiments we exploit the new TPTP…
The decidability of a logical system refers to the existence of an algorithm that can determine whether any given formula in that system is a theorem. In this paper, Harrop's lemma is used to prove the decidability of quantum modal logic.