Publications

Interpreting Knowledge into Belief in the Presence of Negative Introspection
Evan Goris, Technical Report TR-2007005, CUNY Ph.D. Program in Computer Science, 2007
[learn_more caption=”BIBTEX and Abstract”]

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

 

@TechReport{cite-key,
title={Interpreting Knowledge into Belief in the Presence of Negative Introspection},
author={Evan Goris},
year={2007},
number={TR-2007005},
institution={CUNY Ph.D.~Program in Computer Science}
[/learn_more]

Justified Knowledge is Sufficient
Evangelia Antonakos , Technical Report TR-2006004, CUNY Ph.D. Program in Computer Science, 2006
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@TechReport{cite-key,
title={Justified Knowledge is Sufficient},
author={ Evangelia Antonakos },
year={2006},
number={TR-2006004},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

A replacement theorem for LP
Melvin Fitting, Technical Report TR-2006002, CUNY Ph.D. Program in Computer Science, 2006
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@TechReport{cite-key,
title={A replacement theorem for \textsf{LP}},
author={Melvin Fitting},
year={2006},
number={TR-2006002},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Making knowledge explicit: How hard it is
Roman Kuznets and Vladimir Brezhnev, Theoretical Computer Science, 2006
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@Article{cite-key,
title={Making knowledge explicit: How hard it is},
author={Roman Kuznets and Vladimir Brezhnev},
journal={Theoretical Computer Science},
year={2006}
}
[/learn_more]

On Logic of Proofs and Provability
Elena Nogina, presented at the 2005 Summer Meeting of the ASL, abstract published in Bulletin of Symbolic Logic volume 12 issue 2, 2006
[learn_more caption=”BIBTEX”]

 

@Misc{cite-key,
title={On Logic of Proofs and Provability},
author={Elena Nogina},
year={2006},
note={presented at the 2005 Summer Meeting of the ASL, abstract published in Bulletin of Symbolic Logic volume 12 issue 2}
}
[/learn_more]

Propositional Games with Explicit Strategies
Bryan Renne, presented at the 2005 Winter Meeting of the ASL, abstract published in Bulletin of Symbolic Logic, 2006
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@Misc{cite-key,
title={Propositional Games with Explicit Strategies},
author={Bryan Renne},
year={2006},
note={presented at the 2005 Winter Meeting of the ASL, abstract published in Bulletin of Symbolic Logic}
}
[/learn_more]

Semantic cut-elimination for an explicit modal logic
Bryan Renne, In 18th European Summer School in Logic Language and Information, Proceedings of the 11th ESSLLI Student Session, 2006, Malaga, 2006
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@InProceedings{cite-key,
title={Semantic cut-elimination for an explicit modal logic},
author={Bryan Renne},
year={2006},
booktitle={18th European Summer School in Logic Language and Information, Proceedings of the 11th ESSLLI Student Session, 2006, Malaga}
}
[/learn_more]

Explicit Proofs in Formal Provability Logic
Evan Goris, Technical Report TR-2006003, CUNY Ph.D. Program in Computer Science, 2006
[learn_more caption=”BIBTEX and Abstract”]

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

 

@TechReport{cite-key,
title={Explicit Proofs in Formal Provability Logic},
author={Evan Goris},
year={2006},
number={TR-2006003},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Logic of Proofs for Bounded Arithmetic
Evan Goris, In Computer Science – Theory and Applications: First International Computer Science Symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8-12. 2006, volume 3967 of Lecture Notes in Computer Science, pages 191–201, 2006
[learn_more caption=”BIBTEX and Abstract”]

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 S12. 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.

 

@InProceedings{cite-key,
title={Logic of Proofs for Bounded Arithmetic},
author={Evan Goris},
volume={3967},
year={2006},
series={Lecture Notes in Computer Science},
publisher={Elsevier},
booktitle={Computer Science – Theory and Applications: First International Computer Science Symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8-12. 2006},
pages={191–201}
}
[/learn_more]

Existential semantics for modal logic
Sergei N. Artemov, In We Will Show Them: Essays in Honour of Dov Gabbay, pages 19–30, 2005
[learn_more caption=”BIBTEX”]

 

@InCollection{cite-key,
title={Existential semantics for modal logic},
author={Sergei N. Artemov},
volume={1},
year={2005},
publisher={College Publications, London},
booktitle={We Will Show Them: Essays in Honour of Dov Gabbay},
pages={19–30}
}
[/learn_more]

Integration of decision procedures into high-order interactive provers
Yegor Bryukhov, Ph.D. Thesis, CUNY Graduate School, 2005
[learn_more caption=”BIBTEX”]

 

@PhdThesis{cite-key,
title={Integration of decision procedures into high-order interactive provers},
author={Yegor Bryukhov},
year={2005},
school={CUNY Graduate School}
}
[/learn_more]

Automatic Proof Search in Logic of Justified Common Knowledge
Yegor Bryukhov, In Proceedings of Methods for Modalities Workshop 2005, pages 187–201, 2005
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={Automatic Proof Search in Logic of Justified Common Knowledge},
author={Yegor Bryukhov},
year={2005},
publisher={Humboldt University},
booktitle={Proceedings of Methods for Modalities Workshop 2005},
pages={187–201}
}
[/learn_more]

A logic of explicit knowledge
Melvin Fitting, In The Logica Yearbook 2004, pages 11–22, 2005
[learn_more caption=”BIBTEX”]

 

@InCollection{cite-key,
title={A logic of explicit knowledge},
author={Melvin Fitting},
year={2005},
publisher={Filosofia},
booktitle={The Logica Yearbook 2004},
pages={11–22}
}
[/learn_more]

Referential Logic of Proofs
Nikolai V. Krupski, Theoretical Computer Science, (accepted), 2005
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Referential Logic of Proofs},
author={Nikolai V. Krupski},
journal={Theoretical Computer Science},
volume={(accepted)},
year={2005}
}
[/learn_more]

On decidability of the Logic of Proofs with arbitrary constant specifications
Roman Kuznets, Bulletin of Symbolic Logic, 11, 2005
[learn_more caption=”BIBTEX and Abstract”]

 

@Article{cite-key,
title={On decidability of the Logic of Proofs with arbitrary constant specifications},
author={Roman Kuznets},
journal={Bulletin of Symbolic Logic},
volume={11},
year={2005}
}
[/learn_more]

Craig interpolation property for operational logics of proofs
Natalia M. Rubtsova and Tatiana L. Yavorskaya-Sidon, Journal of Applied Non-Classical Logics, 2005 (to appear)
[learn_more caption=”BIBTEX”]

@Article{cite-key,
title={Craig interpolation property for operational logics of proofs},
author={Natalia M. Rubtsova and Tatiana L. Yavorskaya-Sidon},
journal={Journal of Applied Non-Classical Logics},
year={2005},
note={to appear}
}
[/learn_more]

Negative operations on proofs and labels
Tatiana L. Yavorskaya-Sidon, Technical Report Logic Group Preprint Series 239, Department of Philosophy of Utrecht University, 2005
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Negative operations on proofs and labels},
author={Tatiana L. Yavorskaya-Sidon},
year={2005},
number={Logic Group Preprint Series 239},
institution={Department of Philosophy of Utrecht University}
}
[/learn_more]

On Kripke-style semantics for the provability logic of Gödel”s proof predicate with quantifiers on proofs
Rostislav Yavorsky, Technical Report Logic Group Preprint Series 238, Department of Philosophy of Utrecht University, 2005
[learn_more caption=”BIBTEX and Abstract”]

 

@TechReport{cite-key,
title={On Kripke-style semantics for the provability logic of G\”odel”s proof predicate with quantifiers on proofs},
author={Rostislav Yavorsky},
year={2005},
number={Logic Group Preprint Series 238},
institution={Department of Philosophy of Utrecht University}
}
[/learn_more]

The Basic Intuitionistic Logic of Proofs
Sergei N. Artemov and Rosalie Iemhoff, Technical Report TR-2005002, CUNY Ph.D. Program in Computer Science, 2005
[learn_more caption=”BIBTEX and Abstract”]

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

 

@TechReport{cite-key,
title={The Basic Intuitionistic Logic of Proofs},
author={Sergei N. Artemov and Rosalie Iemhoff},
year={2005},
number={TR-2005002},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

On Epistemic Logic with Justification
Sergei N. Artemov and Elena Nogina, In Theoretical Aspects of Rationality and Knowledge Proceedings of the Tenth Conference (TARK 2005), June 10-12, 2005, Singapore, pages 279–294, 2005
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@InProceedings{cite-key,
title={On Epistemic Logic with Justification},
author={Sergei N. Artemov and Elena Nogina},
year={2005},
publisher={National University of Singapore},
booktitle={Theoretical Aspects of Rationality and Knowledge Proceedings of the Tenth Conference (TARK 2005), June 10-12, 2005, Singapore},
pages={279–294}
}
[/learn_more]

Basic Systems of Epistemic Logic with Justifications
Sergei N. Artemov and Elena Nogina, Technical Report TR-2005004, CUNY Ph.D. Program in Computer Science, 2005
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Basic Systems of Epistemic Logic with Justifications},
author={Sergei N. Artemov and Elena Nogina},
year={2005},
number={TR-2005004},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Introducing justification to epistemic logic
Sergei N. Artemov and Elena Nogina, Journal of Logic and Computation, 15(6):1059–1073, 2005
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Introducing justification to epistemic logic},
author={Sergei N. Artemov and Elena Nogina},
journal={Journal of Logic and Computation},
volume={15},
year={2005},
number={6},
pages={1059–1073}
}
[/learn_more]

The Logic of Proofs, Semantically
Melvin Fitting, Annals of Pure and Applied Logic, 132:1–25, 2005
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={The Logic of Proofs, Semantically},
author={Melvin Fitting},
journal={Annals of Pure and Applied Logic},
volume={132},
year={2005},
pages={1–25}
}
[/learn_more]

Making knowledge explicit: How hard it is
Roman Kuznets and Vladimir Brezhnev, Technical Report TR-2005003, CUNY Ph.D. Program in Computer Science, 2005
[learn_more caption=”BIBTEX and Abstract”]

 

@TechReport{cite-key,
title={Making knowledge explicit: How hard it is},
author={Roman Kuznets and Vladimir Brezhnev},
year={2005},
number={TR-2005003},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Logic of Proofs for Bounded Arithmetic
Evan Goris, Technical Report TR-2005011, CUNY Ph.D. Program in Computer Science, 2005
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Logic of Proofs for Bounded Arithmetic},
author={Evan Goris},
year={2005},
number={TR-2005011},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Kolmogorov and Gödel’s approach to intuitionistic logic: current developments
Sergei N. Artemov, Russian Mathematical Surveys, 59(2):203–229, 2004
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Kolmogorov and G\”odel’s approach to intuitionistic logic: current developments},
author={Sergei N. Artemov},
journal={Russian Mathematical Surveys},
volume={59},
year={2004},
number={2},
pages={203–229}
}
[/learn_more]

Intuitionistic Logic with Classical Atoms
Hidenori Kurokawa, Technical Report TR-2004003, CUNY Ph.D. Program in Computer Science, 2004
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Intuitionistic Logic with Classical Atoms},
author={Hidenori Kurokawa},
year={2004},
number={TR-2004003},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Implementing the Calculus of Inductive Constructions in the MetaPRL Framework
Natalia Novak and Yegor Bryukhov, In 17th International Conference on Theorem Proving in Higher Order Logics, volume 3233 of Lecture Notes in Computer Science, pages 153–164, 2004
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@InProceedings{cite-key,
title={Implementing the Calculus of Inductive Constructions in the \textsf{MetaPRL} Framework},
author={Natalia Novak and Yegor Bryukhov},
volume={3233},
year={2004},
series={Lecture Notes in Computer Science},
publisher={Springer},
booktitle={17th International Conference on Theorem Proving in Higher Order Logics},
pages={153–164}
}
[/learn_more]

Evidence-Based Common Knowledge
Sergei N. Artemov, Technical Report TR-2004018, CUNY Ph.D. Program in Computer Science, 2004
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Evidence-Based Common Knowledge},
author={Sergei N. Artemov},
year={2004},
number={TR-2004018},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Provability Logic
Sergei N. Artemov and Lev D. Beklemishev, In Handbook of Philosophical Logic, pages 229–403, 2004
[learn_more caption=”BIBTEX and Abstract”]

 

@InCollection{cite-key,
title={Provability Logic},
author={Sergei N. Artemov and Lev D. Beklemishev},
volume={13},
year={2004},
publisher={Kluwer},
booktitle={Handbook of Philosophical Logic},
pages={229–403}
}
[/learn_more]

Logic of Knowledge with Justifications from the Provability Perspective
Sergei N. Artemov and Elena Nogina, Technical Report TR-2004011, CUNY Ph.D. Program in Computer Science, 2004
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Logic of Knowledge with Justifications from the Provability Perspective},
author={Sergei N. Artemov and Elena Nogina},
year={2004},
number={TR-2004011},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Semantics and Tableaus for LPS4
Melvin Fitting, Technical Report TR-2004016, CUNY Ph.D. Program in Computer Science, 2004
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Semantics and Tableaus for \textsf{LPS4}},
author={Melvin Fitting},
year={2004},
number={TR-2004016},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Quantified LP
Melvin Fitting, Technical Report TR-2004019, CUNY Ph.D. Program in Computer Science, 2004
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Quantified \textsf{LP}},
author={Melvin Fitting},
year={2004},
number={TR-2004019},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Tableaux for the logic of proofs
Bryan Renne, Technical Report TR-2004001, CUNY Ph.D. Program in Computer Science, 2004
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Tableaux for the logic of proofs},
author={Bryan Renne},
year={2004},
number={TR-2004001},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant
Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, and Aleksey Nogin, In 16th International Conference on Theorem Proving in Higher Order Logics, volume 2758 of Lecture Notes in Computer Science, pages 29–39, 2003
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={Implementing and Automating Basic Number Theory in {\textsf{MetaPRL}} Proof Assistant},
author={Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, and Aleksey Nogin},
volume={2758},
year={2003},
series={Lecture Notes in Computer Science},
publisher={Springer},
booktitle={16th International Conference on Theorem Proving in Higher Order Logics},
pages={29–39}
}
[/learn_more]

A Semantics for the Logic of Proofs
Melvin Fitting, Technical Report TR-2003012, CUNY Ph.D. Program in Computer Science, 2003
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={A Semantics for the Logic of Proofs},
author={Melvin Fitting},
year={2003},
number={TR-2003012},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

A Semantic Proof of the Realizability of Modal Logic in the Logic of Proofs
Melvin Fitting, Technical Report TR-2003010, CUNY Ph.D. Program in Computer Science, 2003
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={A Semantic Proof of the Realizability of Modal Logic in the Logic of Proofs},
author={Melvin Fitting},
year={2003},
number={TR-2003010},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

On the Complexity of the Reflected Logic of Proofs
Nikolai V. Krupski, Technical Report TR-2003007, CUNY Ph.D. Program in Computer Science, 2003
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={On the Complexity of the Reflected Logic of Proofs},
author={Nikolai V. Krupski},
year={2003},
number={TR-2003007},
institution={CUNY Ph.D.~Program in Computer Science}
}
[/learn_more]

The single-conclusion proof logic and inference rules specification
Nikolai V. Krupski, Annals of Pure and Applied Logic, 113(1-3):181–201, 2002
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={The single-conclusion proof logic and inference rules specification},
author={Nikolai V. Krupski},
journal={Annals of Pure and Applied Logic},
volume={113},
year={2002},
number={1-3},
pages={181–201}
}
[/learn_more]

Provability logics with quantifiers on proofs
Rostislav Yavorsky, Annals of Pure and Applied Logic, 113(1-3):373–387, 2002
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Provability logics with quantifiers on proofs},
author={Rostislav Yavorsky},
journal={Annals of Pure and Applied Logic},
volume={113},
year={2002},
number={1-3},
pages={373–387}
}
[/learn_more]

Logic of Proofs and Provability
Tatiana L. Yavorskaya-Sidon, Annals of Pure and Applied Logic, 113(1-3):345–372, 2002
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Logic of Proofs and Provability},
author={Tatiana L. Yavorskaya-Sidon},
journal={Annals of Pure and Applied Logic},
volume={113},
year={2002},
number={1-3},
pages={345–372}
}
[/learn_more]

Reflective λ-calculus
Jesse Alt and Sergei N. Artemov, In Proceedings of the Dagstuhl-Seminar on Proof Theory in Computer Science, volume 2183 of Lecture Notes in Computer Science, pages 22–37, 2001
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={Reflective $\lambda$-calculus},
author={Jesse Alt and Sergei N. Artemov},
volume={2183},
year={2001},
series={Lecture Notes in Computer Science},
publisher={Springer},
booktitle={Proceedings of the Dagstuhl-Seminar on Proof Theory in Computer Science},
pages={22–37}
}
[/learn_more]

On the first order logic of proofs
Sergei N. Artemov and Tatiana L. Yavorskaya-Sidon, Moscow Mathematical Journal, 1:475–490, 2001
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={On the first order logic of proofs},
author={Sergei N. Artemov and Tatiana L. Yavorskaya-Sidon},
journal={Moscow Mathematical Journal},
volume={1},
year={2001},
pages={475–490}
}
[/learn_more]

Operations on proofs that can be specified by means of modal logic
Sergei N. Artemov, In Advances in Modal Logic. Volume 2, pages 59–72, 2001
[learn_more caption=”BIBTEX”]

 

@InCollection{cite-key,
title={Operations on proofs that can be specified by means of modal logic},
author={Sergei N. Artemov},
year={2001},
publisher={CSLI Publications},
booktitle={Advances in Modal Logic. Volume 2},
pages={59–72}
}
[/learn_more]

On the Logic of Proofs
Vladimir Brezhnev, In 13th European Summer School in Logic Language and Information, Proceedings of the 6th ESSLLI Student Session, 2001, Helsinki, pages 35–46, 2001
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={On the Logic of Proofs},
author={Vladimir Brezhnev},
year={2001},
booktitle={13th European Summer School in Logic Language and Information, Proceedings of the 6th ESSLLI Student Session, 2001, Helsinki},
pages={35–46}
}
[/learn_more]

Explicit Provability and Constructive Semantics
Sergei N. Artemov, Bulletin of Symbolic Logic, 7(1):1–36, 2001
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Explicit Provability and Constructive Semantics},
author={Sergei N. Artemov},
journal={Bulletin of Symbolic Logic},
volume={7},
year={2001},
number={1},
pages={1–36}
}
[/learn_more]

On explicit counterparts of modal logics
Vladimir Brezhnev, Technical Report CFIS 2000-05, Cornell University, 2000
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={On explicit counterparts of modal logics},
author={Vladimir Brezhnev},
year={2000},
number={CFIS 2000-05},
institution={Cornell University}
}
[/learn_more]

On the logic of the standard proof predicate
Rostislav Yavorsky, In Computer Science Logic 2000, volume 1862 of Lecture Notes in Computer Science, pages 527–541, 2000
[learn_more caption=”BIBTEX”]

 

@InCollection{cite-key,
title={On the logic of the standard proof predicate},
author={Rostislav Yavorsky},
volume={1862},
year={2000},
series={Lecture Notes in Computer Science},
publisher={Springer},
booktitle={Computer Science Logic 2000},
pages={527–541}
}
[/learn_more]

On the Complexity of Explicit Modal Logic
Roman Kuznets, In Proceedings of the 14th International Conference of Computer Science Logic, volume 1862 of Lecture Notes in Computer Science, pages 371–383, 2000
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={On the Complexity of Explicit Modal Logic},
author={Roman Kuznets},
volume={1862},
year={2000},
series={Lecture Notes in Computer Science},
booktitle={Proceedings of the 14th International Conference of Computer Science Logic},
pages={371–383}
}
[/learn_more]

Epistemic logic with justifications
Sergei N. Artemov, E. Kazakov, and D. Shapiro, Technical Report CFIS 99-12, Cornell University, 1999
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Epistemic logic with justifications},
author={Sergei N. Artemov, E. Kazakov, and D. Shapiro},
year={1999},
number={CFIS 99-12},
institution={Cornell University}
}
[/learn_more]

Deep isomorphism of modal derivations and lambda-terms
Sergei N. Artemov, In Proceedings of the Workshop Intuitionistic Modal Logic and Applications, 1999 (Tech Report CFIS 99-07, Cornell University)
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={Deep isomorphism of modal derivations and lambda-terms},
author={Sergei N. Artemov},
year={1999},
note={Tech Report CFIS 99-07, Cornell University},
publisher={Trento, Italy},
booktitle={Proceedings of the Workshop Intuitionistic Modal Logic and Applications}
}
[/learn_more]

On explicit reflection in theorem proving and formal verification
Sergei N. Artemov, In Automated Deduction – CADE-16. Proceedings of the 16th International Conference on Automated Deduction, Trento, Italy, July 1999, volume 1632 of Lecture Notes in Artificial Intelligence, pages 267–281, 1999
[learn_more caption=”BIBTEX”]


@InProceedings{cite-key,
title={On explicit reflection in theorem proving and formal verification},
author={Sergei N. Artemov},
volume={1632},
year={1999},
series={Lecture Notes in Artificial Intelligence},
publisher={Springer},
booktitle={Automated Deduction – CADE-16. Proceedings of the 16th International Conference on Automated Deduction, Trento, Italy, July 1999},
pages={267–281}
}
[/learn_more]

An Operational Logic of Proofs with Positive and Negative Information
Duccio Luchi and Franco Montagna, Studia Logica, 63(1):7–25, 1999
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={An Operational Logic of Proofs with Positive and Negative Information},
author={Duccio Luchi and Franco Montagna},
journal={Studia Logica},
volume={63},
year={1999},
number={1},
pages={7–25}
}
[/learn_more]

Logic of Proofs: a Unified Semantics for Modality and λ-terms
Sergei N. Artemov, Technical Report CFIS 98-06, Cornell University, 1998
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Logic of Proofs: a Unified Semantics for Modality and $\lambda$-terms},
author={Sergei N. Artemov},
year={1998},
number={CFIS 98-06},
institution={Cornell University}
}
[/learn_more]

Explicit provability: the intended semantics for intuitionistic and modal logic
Sergei N. Artemov, Technical Report CFIS 98-10, Cornell University, 1998
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Explicit provability: the intended semantics for intuitionistic and modal logic},
author={Sergei N. Artemov},
year={1998},
number={CFIS 98-10},
institution={Cornell University}
}
[/learn_more]

Craig interpolation property for operational logics of proofs
Tatiana L. Yavorskaya-Sidon, Vestnik Moskovskogo Universiteta. Ser. 1 Mat., Mech., 53(2):34–38, 1998 (In Russian. English translation in: \em Moscow University Mathematics Bulletin)
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Craig interpolation property for operational logics of proofs},
author={Tatiana L. Yavorskaya-Sidon},
journal={Vestnik Moskovskogo Universiteta. Ser. 1 Mat., Mech.},
volume={53},
year={1998},
number={2},
note={In Russian. English translation in: \em Moscow University Mathematics Bulletin},
pages={34–38}
}
[/learn_more]

Proof realizations of typed λ-calculi
Sergei N. Artemov, Technical Report MSI 95-02, Cornell University, 1997
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Proof realizations of typed $\lambda$-calculi},
author={Sergei N. Artemov},
year={1997},
number={MSI 95-02},
institution={Cornell University}
}
[/learn_more]

Operational Logic of Proofs with Functionality Condition on Proof Predicate
Nikolai V. Krupski, In Logical Foundations of Computer Science ’97, Yaroslavl’, volume 1234 of Lecture Notes in Computer Science, pages 167–177, 1997
[learn_more caption=”BIBTEX”]

 

@InCollection{cite-key,
title={Operational Logic of Proofs with Functionality Condition on Proof Predicate},
author={Nikolai V. Krupski},
volume={1234},
year={1997},
series={Lecture Notes in Computer Science},
publisher={Springer},
booktitle={Logical Foundations of Computer Science ’97, Yaroslavl’},
pages={167–177}
}
[/learn_more]

Provability Logic with Operations on Proofs
Tatiana L. Yavorskaya-Sidon, In Logical Foundations of Computer Science “97, Yaroslavl”, volume 1234 of Lecture Notes in Computer Science, pages 342–353, 1997
[learn_more caption=”BIBTEX”]

 

@InCollection{cite-key,
title={Provability Logic with Operations on Proofs},
author={Tatiana L. Yavorskaya-Sidon},
volume={1234},
year={1997},
series={Lecture Notes in Computer Science},
publisher={Springer},
booktitle={Logical Foundations of Computer Science “97, Yaroslavl”},
pages={342–353}
}
[/learn_more]

Models for the logic of proofs
Alexey Mkrtychev, In Logical foundations of computer science, volume 1234 of Lecture Notes in Computer Science, pages 266–275, 1997
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={Models for the logic of proofs},
author={Alexey Mkrtychev},
volume={1234},
year={1997},
series={Lecture Notes in Computer Science},
booktitle={Logical foundations of computer science},
pages={266–275}
}
[/learn_more]

Provability Logic with Operations on Proofs
Tatiana L. Yavorskaya-Sidon, In Proceedings of the 4th International Symposium on Logical Foundations of Computer Science, volume 1234 of lncs, pages 342–353, 1997
[learn_more caption=”BIBTEX”]

 

@InCollection{cite-key,
title={Provability Logic with Operations on Proofs},
author={Tatiana L. Yavorskaya-Sidon},
volume={1234},
year={1997},
series={lncs},
publisher={Springer Verlag},
booktitle={Proceedings of the 4th International Symposium on Logical Foundations of Computer Science},
pages={342–353}
}
[/learn_more]

Data storage interpretation of labeled modal logic
Sergei N. Artemov and Nikolai V. Krupski, Annals of Pure and Applied Logic, 78(1):57–71, 1996
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Data storage interpretation of labeled modal logic},
author={Sergei N. Artemov and Nikolai V. Krupski},
journal={Annals of Pure and Applied Logic},
volume={78},
year={1996},
number={1},
pages={57–71}
}
[/learn_more]

Grzegorczyk logic with arithmetical proof operators
Elena Nogina, Fundamental and Applied Mathematics, 2(2):483–499, 1996
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Grzegorczyk logic with arithmetical proof operators},
author={Elena Nogina},
journal={Fundamental and Applied Mathematics},
volume={2},
year={1996},
number={2},
pages={483–499}
}
[/learn_more]

Operational Modal Logic
Sergei N. Artemov, Technical Report MSI 95-29, Cornell University, 1995
[learn_more caption=”BIBTEX”]

 

@TechReport{cite-key,
title={Operational Modal Logic},
author={Sergei N. Artemov},
year={1995},
number={MSI 95-29},
institution={Cornell University}
}
[/learn_more]

Referential data structures and labeled modal logic
Sergei N. Artemov and Vladimir Krupski, In Logical Foundations of Computer Science’ 94, St. Petersburg, volume 813 of Lecture Notes in Computer Science, pages 23–33, 1994
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={Referential data structures and labeled modal logic},
author={Sergei N. Artemov and Vladimir Krupski},
volume={813},
year={1994},
series={Lecture Notes in Computer Science},
publisher={Springer},
booktitle={Logical Foundations of Computer Science’ 94, St. Petersburg},
pages={23–33}
}
[/learn_more]

Logic of proofs with the strong provability operator
Elena Nogina, Technical Report ML-94-10, ILLC, 1994
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@TechReport{cite-key,
title={Logic of proofs with the strong provability operator},
author={Elena Nogina},
year={1994},
number={ML-94-10},
institution={ILLC}
}
[/learn_more]

The Basic Logic of Proofs
Tyko Straßen, Ph.D. Thesis, University of Bern, 1994
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@PhdThesis{cite-key,
title={The Basic Logic of Proofs},
author={Tyko Stra\ssen},
year={1994},
school={University of Bern}
}
[/learn_more]

Syntactical Models and Fixed Points for the Basic Logic of Proofs
Tyko Straßen, Annals of Mathematics and Artificial Intelligence, 12(3-4):291–321, 1994
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@Article{cite-key,
title={Syntactical Models and Fixed Points for the Basic Logic of Proofs},
author={Tyko Stra\ssen},
journal={Annals of Mathematics and Artificial Intelligence},
volume={12},
year={1994},
number={3-4},
pages={291–321}
}
[/learn_more]

Logic of Proofs
Sergei N. Artemov, Annals of Pure and Applied Logic, 67:29–59, 1994
[learn_more caption=”BIBTEX”]

 

@Article{cite-key,
title={Logic of Proofs},
author={Sergei N. Artemov},
journal={Annals of Pure and Applied Logic},
volume={67},
year={1994},
pages={29–59}
}
[/learn_more]

Functionality in the basic logic of proofs
Sergei N. Artemov and Tyko Straßen, Technical Report IAM 93-004, Department of Computer Science, University of Bern, 1993
[learn_more caption=”BIBTEX and Abstract”]

 

@TechReport{cite-key,
title={Functionality in the basic logic of proofs},
author={Sergei N. Artemov and Tyko Stra\ssen},
year={1993},
number={IAM 93-004},
institution={Department of Computer Science, University of Bern}
}
[/learn_more]

The logic of the Gödel proof predicate
Sergei N. Artemov and Tyko Straßen, In Computational Logic and Proof Theory. Third Kurt Gödel Colloquium, KGC’93. Brno, Chech Republic, August 1993. Proceedings, volume 713 of Lecture Notes in Computer Science, pages 71–82, 1993
[learn_more caption=”BIBTEX”]

 

@InProceedings{cite-key,
title={The logic of the G\”odel proof predicate},
author={Sergei N. Artemov and Tyko Stra\ssen},
volume={713},
year={1993},
series={Lecture Notes in Computer Science},
publisher={Springer},
booktitle={Computational Logic and Proof Theory. Third Kurt G\”odel Colloquium, KGC’93. Brno, Chech Republic, August 1993. Proceedings},
pages={71–82}
}
[/learn_more]

Functionality in the Basic Logic of Proofs
Sergei N. Artemov and Tyko Straßen, Technical Report IAM-93-004, Institute of Computer Science and Applied Mathematics, University of Bern, Switzerland, 1993
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@TechReport{cite-key,
title={Functionality in the Basic Logic of Proofs},
author={Sergei N. Artemov and Tyko Stra\ssen},
year={1993},
number={IAM-93-004},
institution={Institute of Computer Science and Applied Mathematics, University of Bern, Switzerland}
}
[/learn_more]

Syntactical Models and Fixed Points for the Basic Logic of Proofs
Tyko Straßen, Technical Report IAM-93-020, Institute of Computer Science and Applied Mathematics, University of Bern, Switzerland, 1993
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@TechReport{cite-key,
title={Syntactical Models and Fixed Points for the Basic Logic of Proofs},
author={Tyko Stra\ssen},
year={1993},
number={IAM-93-020},
institution={Institute of Computer Science and Applied Mathematics, University of Bern, Switzerland}
}
[/learn_more]

The Basic Logic of Proofs
Sergei N. Artemov and Tyko Straßen, In Selected papers of the 6th Workshop on Computer Science Logic (CSL-1992), San Miniato, Italy, September 28-October 2, 1992, volume 702 of Lecture Notes in Computer Science, pages 14–28, 1993
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@InProceedings{cite-key,
title={The Basic Logic of Proofs},
author={Sergei N. Artemov and Tyko Stra\ssen},
volume={702},
year={1993},
series={Lecture Notes in Computer Science},
publisher={Springer-Verlag},
booktitle={Selected papers of the 6th Workshop on Computer Science Logic (CSL-1992), San Miniato, Italy, September 28-October 2, 1992},
pages={14–28}
}
[/learn_more]

The Basic Logic of Proofs
Sergei N. Artemov and Tyko Straßen, Technical Report IAM-92-018, Institute of Computer Science and Applied Mathematics, University of Bern, Switzerland, 1992
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@TechReport{cite-key,
title={The Basic Logic of Proofs},
author={Sergei N. Artemov and Tyko Stra\ssen},
year={1992},
number={IAM-92-018},
institution={Institute of Computer Science and Applied Mathematics, University of Bern, Switzerland}
}
[/learn_more]

Kolmogorov’s Logic of Problems and a Provability Interpretation of Intuitionistic Logic
Sergei N. Artemov, In Proceedings of the 3rd Conference on Theoretical Aspects of Reasoning about Knowledge (TARK-1990), Pacific Grove, CA, USA, March 4-7, 1990, pages 257–272, 1990
[learn_more caption=”BIBTEX and Abstract”]

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.

 

@InProceedings{cite-key,
title={Kolmogorov’s Logic of Problems and a Provability Interpretation of Intuitionistic Logic},
author={Sergei N. Artemov},
year={1990},
publisher={Morgan Kaufmann},
booktitle={Proceedings of the 3rd Conference on Theoretical Aspects of Reasoning about Knowledge (TARK-1990), Pacific Grove, CA, USA, March 4-7, 1990},
pages={257–272}
}
[/learn_more]

Leave a Reply

Your email address will not be published. Required fields are marked *