Publications

Abstract: This paper studies a particular interpretation of propositional modal logic into propositional modal logic. Under an epistemic reading of the modality this interpretation can be understood as taking knowledge to be true belief. All normal modal logics of belief that under this definition of knowledge give rise to S5 as the logic of knowledge are determined. And all the normal modal logics of belief that give rise to S4w5 as the logic of knowledge are determined. Among the latter KD45 shows up as a maximal such logic.

Abstract: Three formal approaches to public knowledge are `any fool' knowledge by McCarthy (1970), Common Knowledge by Halpern and Moses (1990), and Justified Knowledge by Artemov (2004). We compare them to mathematically address the observation that the light-weight systems of Justified Knowledge and `any fool knows' suffice to solve standard epistemic puzzles for which heavier solutions based on Common Knowledge are offered by standard textbooks. Specifically we show that epistemic systems with Common Knowledge modality C are conservative with respect to Justified Knowledge systems on formulas F&C(G)=>H, where F, G, and H are C-free. We then notice that formalization of standard epistemic puzzles can be made in the aforementioned form, hence each time there is a solution within a Common Knowledge system, there is a solution in the corresponding Justified Knowledge system.

Abstract: The replacement theorem for classical and normal modal logics is a fundamental tool. It says that if A and B have been proved equivalent, occurrences of A can be replaced by occurrences of B to produce a formula equivalent to the original one. This theorem does not hold for LP Logic of Proofs. A replacement to replacement is not easy to formulate. In this paper we provide one, along with some machinery for working with LP realizations that May prove useful for other things as well.

Abstract: Artemov's logic of proofs LP is a complete calculus of propositions and proofs, which is now becoming a foundation for the evidence-based approach to reasoning about knowledge. Additional atoms in LP have form t:F, read as "t is a proof of F" (or, more generally, as "t is an evidence for F") for an appropriate system of terms t called proof polynomials. In this paper, we answer two well-known questions in this area. One of the main features of LP is its ability to realize modalities in any S4 derivation by proof polynomials thus revealing a statement about explicit evidences encoded in that derivation. We show that the original Artemov's algorithm of building such realizations can produce proof polynomials of exponential length in the size of the initial S4 derivation. We modify the realization algorithm to produce proof polynomials of at most quadratic length. We also found a modal formula, any realization of which necessarily requires self-referential constants of type c:A(c). This demonstrates that the evidence-based reasoning encoded by the modal logic S4 is inherently self-referential.

Abstract: Applying a game-theoretic semantics to a logic gives primacy to considerations of strategy when reasoning about that logic. By internalizing these strategies, the logic can itself reason about strategy. With this interpretation in mind, this paper studies Artemov's Logic of Proofs as a logic of specific, explicit strategies on propositional games.

Abstract: Explicit modal logics have recently been put forth as a means of handling common knowledge in multi-agent systems. These logics have certain proof-theoretic advantages over the usual multi-modal logics, perhaps the most important of which is conventional cut-elimination. The present paper studies a tableau proof system for the most basic explicit modal logic, the Logic of Proofs. Using a certain method to prove the correctness of the tableau system, a semantic proof of cut-elimination falls out naturally. This method is quite general and, with some care, can be extended to a wide range of explicit modal logics.

Abstract: In this paper we answer the question what implicit proof assertions in the provability logic GL can be realized by explicit proof terms. In particular we show that the fragment of GL which can be realized by generalized proof terms of GLA is exactly S4 intersected with GL and equals the fragment that can be realized by proof terms of LP. Additionally we show that the problem of determining which implicit provability assertions in a given modal formula can be made explicit is decidable. In the final sections of this paper we establish the disjunction property for GLA and give an axiomatization for S4 intersected with GL.

Abstract: The logic of proofs is known to be complete for the semantics of proofs in Peano Arithmetic PA. In this paper we present a refinement of this theorem, we will show that we can assure that all the operations on proofs can be realized by feasible, that is PTIME-computable, functions. In particular we will show that the logic of proofs is complete for the semantics of proofs in Buss's bounded arithmetic S¹₂. In view of recent applications of the Logic of Proofs in epistemology this result shows that explicit knowledge in the propositional framework can be made computationally feasible.

Abstract: The langauge of the basic logic of proofs extends the usual propositional language by forming sentences of the sort `x is a proof of F' for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.

Abstract: The true belief components of Plato's tripartite definition of knowledge as justified true belief are represented in formal epistemology by modal logic and its possible worlds semantics. At the same time, the justification component of Plato's definition did not have a formal representation. This paper introduces the notion of justification into formal epistemology. Epistemic logic with justification, along with the usual knowledge operator []F (F is known ), contains assertions t:F (t is a justification for F). We suggest an epistemic semantics which augments Kripke models with a natural Fitting-style treatment of justification assertions t:F. Completeness and some new specific properties of basic systems of epistemic logic with justification are established.

Abstract: The Calculus of Inductive Constructions is an underlying logic of the Coq proof assistant - a widely used mature proof assistant. In this paper we present our work on implementing the Calculus of Inductive Constructions in the MetaPRL logical framework. Rules from the Coq reference manual have quite unrestricted format so we have to make certain design decisions in order to express those rules in the plain Gentzen style supported by MetaPRL. The most complicated case-analysis and fixpoint rules have yet to be implemented. There is a working implementation with rudimentary proof automation; the toy example of inductive definition (parameterized lists) is type-checked.

Abstract: Logics with the strong provability operator "... is true and provable" together with the proof operators "p is a proof of..." are axiomatized. Kripke- style completeness, decidability and arithmetical completeness of these logics are established.

Abstract: Propositional Provability Logic was axiomatized by R. M. Solovay in 1976. This modal logic describes the behavior of the arithmetical operator "A is provable". The aim of these investigations is to provide propositional axiomatizations of the predicates "p is a proof of A""p is a proof which contains A" and "p is a program which computes A" using the same semantics. The presented systems, called the Basic Logic of Proofs, are first proved to be sound and complete with respect to arithmetical interpretations. Decidability is a consequence of a semantical cut elimination theorem. Moreover, appropriate syntactical models for the Basic Logic of Proofs are defined, which are closely related to canonical models. Finally, some general principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.

Abstract: The Basic Logic of Proofs provides propositional axiomatizations of the predicate "$p$ is a proof of $A$" using the same semantics as the Provability Logic GL. In this paper syntactical models for the Basic Logic of Proofs are described, which are closely related to canonical models. For each system of this class of logics soundness and completeness are proved. Moreover, some principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.

Abstract: This report describes the elimination of the injectivity restriction for functional arithmetical interpretations as used in the systems $\mathcalPF$ and $\mathcalPFM$ in the Basic Logic of Proofs. An appropriate axiom system $\mathcalPU$ in a language with operators "$x$ is a proof of $y$" is defined and proved to be sound and complete with respect to all arithmetical interpretations based on functional proof predicates. Unification plays a major role in the formulation of the new axioms.

Abstract: This report describes syntactical models for the Basic Logic of Proofs, which are closely related to canonical models. For each system of this class of logics soundness and completeness are proved. Moreover, some basic principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.

Abstract: Propositional Provability Logic was axiomatized in [5]. This logic describes the behaviour of the arithmetical operator "$y$ is provable". The aim of the current paper is to provide propositional axiomatizations of the predicate "$x$ is a proof of $y$" by means of modal logic, with the intention of meeting some of the needs of computer science.

Abstract: Propositional Provability Logic was axiomatized in [7]. This logic describes the behaviour of the arithmetical operator "y is provable". The aim of the current paper is to provide propositional axiomatizations of the predicate "x is a proof of y" by means of modal logic, with the intention of meeting some of the needs of computer science.

Abstract: In 1932 A. N. Kolmogorov suggested an interpretation of intuitionistic logic Int as a "logic of problems". Then K. Gödel in 1933 offered a "provability" understanding of problems, thus, providing an abstract "provability" interpretation for Int via a modal logic S4. Later papers by J. C. C. McKinsey, A. Tarski, A. Grzegorczyk, R. Solovay, A. V. Kuznetsov, A. Yu. Muravitskii, R. Goldblatt, G. Boolos imply that this provabllity interpretation of Int is complete if one decodes Gödel modality [] for an "abstract provability" in the following way: []Q = Q & Pr[Q], where Pr[Q] is the standard provability predicate for Peano arithmetic. The paper shows that the definition of []Q as Q & Pr[Q] is (in a certain sense) the only possible one. The Uniform Completeness Theorem for provabllity logics is extended to Int and other logics having Gödelian provability interpretation. The first order logics having provability interpretation are considered.