@comment{{This file has been generated by bib2bib 1.95}}
@comment{{Command line: bib2bib -oc JLBnonoteentries -ob JLBnonote.bib -c "not $key:'nonote'" JLBibliography.bib}}
@techreport{Ach10TR,
author = {Antonis Achilleos},
title = {A Complexity Question in Justification Logic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2010},
number = {TR--2010014},
month = dec,
note = {Later version published as~\cite{Ach11WoLLIC}},
http = {http://tr.cs.gc.cuny.edu/tr/techreport.php?id=410},
pdf = {http://tr.cs.gc.cuny.edu/tr/files/TR-2010014.pdf},
abstract = {Bounds for the computational complexity of major justification logics were found in papers by Buss, N.~Krupski, Kuznets, and Milnikel:
logics~J, J4, JT, LP and~JD, were established to be $\Sigma_2^p$-complete.
A corresponding lower bound is also known for~JD4,
the system that includes the consistency axiom and positive introspection.
However, no upper bound has been established so far for this logic.
Here, the missing upper bound for the complexity of~JD4 is established through an alternating algorithm.
It is shown that using Fitting models of only two worlds is adequate to describe~JD4;
this helps to produce an effective tableau procedure and essentially is what distinguishes the new algorithm from existing ones.}
}
@incollection{Ach11WoLLIC,
author = {Antonis Achilleos},
title = {A Complexity Question in Justification Logic},
booktitle = {{L}ogic, {L}anguage, {I}nformation and {C}omputation, 18th~International {W}orkshop, {WoLLIC~2011},
{P}hiladelphia, {PA}, {USA}, {M}ay 18--20, 2011, Proceedings},
publisher = {Springer},
year = {2011},
editor = {Lev D. Beklemishev and Ruy de Queiroz},
volume = {6642},
series = {Lecture Notes in Artificial Intelligence},
pages = {8--19},
doi = {10.1007/978-3-642-20920-8_7},
conference = {http://wollic.org/wollic2011/},
keywords = {Justification Logic, Computational Complexity, Satisfiability},
abstract = {Bounds for the computational complexity of major justification logics were found in papers by Buss, N.~Krupski, Kuznets, and Milnikel:
logics~J, J4, JT, LP and~JD, were established to be $\Sigma_2^p$-complete.
A corresponding lower bound is also known for~JD4, the system that includes the consistency axiom and positive introspection.
However, no upper bound has been established so far for this logic.
Here, the missing upper bound for the complexity of~JD4 is established through an alternating algorithm.
It is shown that using Fitting models of only two worlds is adequate to describe~JD4;
this helps to produce an effective tableau procedure and essentially is what distinguishes the new algorithm from existing ones.}
}
@incollection{AltArt01PTCS,
author = {Jesse Alt and Sergei [N.] Artemov},
title = {Reflective {$\lambda$}-Calculus},
booktitle = {{P}roof {T}heory in {C}omputer {S}cience, International Seminar, {PTCS} 2001,
{D}agstuhl {C}astle, {G}ermany, {O}ctober 7--12, 2001, Proceedings},
year = {2001},
editor = {Reinhard Kahle and Peter Schroeder-Heister and Robert St{\"{a}}rk},
volume = {2183},
series = {Lecture Notes in Computer Science},
pages = {22--37},
publisher = {Springer},
doi = {10.1007/3-540-45504-3_2},
conference = {http://www.dagstuhl.de/01411},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/LNCS2183.ps},
abstract = {We introduce a general purpose typed $\lambda$-calculus~$\mathbf{\lambda^{\infty}}$ which contains intuitionistic logic, is capable of internalizing its own derivations as $\lambda$-terms and
yet enjoys strong normalization with respect to a natural reduction system.
In particular, $\mathbf{\lambda^{\infty}}$~subsumes the typed $\lambda$-calculus.
The Curry-Howard isomorphism converting intuitionistic proofs into $\lambda$-terms is a simple instance of the internalization property of~$\mathbf{\lambda^{\infty}}$.
The standard semantics of~$\mathbf{\lambda^{\infty}}$ is given by a proof system with proof checking capacities.
The system~$\mathbf{\lambda^{\infty}}$ is a theoretical prototype of reflective extensions of a broad class of type-based systems in programming languages, provers, AI and knowledge representation, etc.}
}
@inproceedings{Ant05PLS,
author = {Evangelia Antonakos},
title = {Comparing Justified and Common Knowledge},
booktitle = {Proceedings of the 5th~{P}anhellenic {L}ogic {S}ymposium},
year = {2005},
month = jul # { 25--28,},
address = {Athens, Greece},
publisher = {University of {A}thens},
pages = {19--25},
conference = {http://cgi.di.uoa.gr/~pls5/},
pdf = {http://www.softlab.ntua.gr/~nickie/tmp/pls5/antonakos.pdf},
abstract = {What is public information in a multiagent logic of knowledge such as $\mathsf{T}_n$, $\mathsf{S4}_n$ or~$\mathsf{S5}_n$?
Traditionally this notion has been captured by \emph{common knowledge}, which is an epistemic operator $C\varphi$ given roughly as $\wedge_{n=0}^{\infty} E^n\varphi$
where $E\varphi = K_1\varphi \land K_2\varphi \land \ldots \land K_n\varphi$ (\emph{everyone knows}~$\varphi$) and $K_i$~is an individual agent's knowledge operator.
In common knowledge systems~$\mathsf{T}_n^C$, $\mathsf{S4}_n^C$, and~$\mathsf{S5}_n^C$, $C$~depends directly on the agents' logic~([FagHalMosVar95]).
A stronger notion of public information is introduced in~\cite{Art04TR} with the new epistemic operator~$J$.
This provides \emph{evidence-based common knowledge} for which~$J \varphi$ ($\varphi$~\emph{is justified})
asserts that there is access to a proof of~$\varphi$.
Evidence-based systems are more flexible than their $C$~counterparts
as the logic for~$J$ can be chosen independently from that of the agents.
The paper~\cite{Art04TR} considers evidence-based systems~$\mathsf{T}_n^J$, $\mathsf{S4}_n^J$, and~$\mathsf{S5}_n^J$
obtained from the base logics~$\mathsf{T}_n$, $\mathsf{S4}_n$, and~$\mathsf{S5}_n$
by adding a copy of~$\mathsf{S4}$ for~$J$ and a connection principle $J\varphi \to K_i\varphi$,
$i = 1, \ldots, n$.
In this paper we compare common knowledge and justified knowledge in a canonical situation
of the base logic~$\mathsf{S4}$ and specify an exact logic principle that distinguishes them.
Let \textsf{I.A.}~stand for the ``Induction Axiom''
\[
\varphi \land J(\varphi \land E\varphi) \to J\varphi.
\]
\textbf{Theorem}. $\mathsf{S4}_n^C \equiv (\mathsf{S4_n^J} + \textsf{I.A.})^*$,
\emph{where $^*$~is replacing~$J$ by~$C$}.\\
This theorem provides an alternative formulation for~$\mathsf{S4}_n^C$.}
}
@techreport{Ant06TR,
author = {Evangelia Antonakos},
title = {Justified Knowledge is Sufficient},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2006},
number = {TR--2006004},
month = apr,
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2006004.ps},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2006004.pdf},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=180},
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 $\chi \land C\varphi \to \psi$,
where $\chi$, $\varphi$, and~$\psi$ 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.}
}
@inproceedings{Ant06LC,
author = {Evangelia Antonakos},
title = {Comparing justified and common knowledge},
booktitle = {2005~Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'05,
{A}thens, {G}reece, {J}uly~28--{A}ugust~3, 2005},
year = {2006},
volume = {12(2)},
series = {Bulletin of Symbolic Logic},
pages = {323--324},
month = jun,
publisher = {Association for Symbolic Logic},
conference = {http://www.math.uoa.gr/lc2005/},
note = {Abstract},
ps = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps},
doi = {10.2178/bsl/1146620064},
abstract = {What is public information in a multiagent logic of knowledge such as $\mathsf{T}_n$, $\mathsf{S4}_n$ or~$\mathsf{S5}_n$?
Traditionally this notion has been captured by \emph{common knowledge}, which is an epistemic operator $C\varphi$ given roughly as $\wedge_{n=0}^{\infty} E^n\varphi$
where $E\varphi = K_1\varphi \land K_2\varphi \land \cdots \land K_n\varphi$ (\emph{everyone knows}~$\varphi$) and $K_i$s are individual agent's knowledge operators.
In common knowledge systems~$\mathsf{T}_n^C$, $\mathsf{S4}_n^C$, and~$\mathsf{S5}_n^C$, $C$~depends directly on the agents' logic~([FagHalMosVar95]).
A stronger notion of public information is introduced in~\cite{Art04TR} with the new epistemic operator~$J$.
This provides \emph{evidence-based common knowledge} for which~$J \varphi$ ($\varphi$~\emph{is justified})
asserts that there is access to a proof of~$\varphi$.
Evidence-based systems are more flexible than their $C$~counterparts
as the logic for~$J$ can be chosen independently from that of the agents.
The paper~\cite{Art04TR} considers evidence-based systems~$\mathsf{T}_n^J$, $\mathsf{S4}_n^J$, and~$\mathsf{S5}_n^J$
obtained from the base logics~$\mathsf{T}_n$, $\mathsf{S4}_n$, and~$\mathsf{S5}_n$
by adding a copy of~$\mathsf{S4}$ for~$J$ and a connection principle $J\varphi \to K_i\varphi$,
$i = 1, \ldots, n$.
In this paper we compare common knowledge and justified knowledge in a canonical situation
of the base logic~$\mathsf{S4}$ and specify an exact logic principle that distinguishes them.
Let \textsf{I.A.}~stand for the ``Induction Axiom''
\[
\varphi \land J(\varphi \to E\varphi) \to J\varphi.
\]
\textbf{Theorem}. $\mathsf{S4}_n^C \equiv (\mathsf{S4_n^J} + \textsf{I.A.})^*$,
\emph{where $^*$~is replacing~$J$ by~$C$}.\\
This theorem provides an alternative formulation for~$\mathsf{S4}_n^C$.}
}
@inproceedings{Ant07ASL,
author = {Evangelia Antonakos},
title = {Epistemic logic with common and justified common knowledge},
booktitle = {2007 Annual Meeting of the Association for Symbolic Logic,
{U}niversity of {F}lorida, {G}ainesville, {F}lorida, {M}arch 10--13, 2007},
year = {2007},
volume = {13(3)},
series = {Bulletin of Symbolic Logic},
pages = {402--403},
month = sep,
publisher = {Association for Symbolic Logic},
note = {Abstract},
conference = {http://www.math.ufl.edu/~jal/logicyear/asl/},
ps = {http://www.math.ucla.edu/~asl/bsl/1303/1303-005.ps},
doi = {10.2178/bsl/1186666153},
abstract = {A multi-agent epistemic logic~$\mathbf{S4}_n^{CJ}$ is defined
which encompasses both traditional Common Knowledge~$C$ (cf.~[FagHalMosVar95, MeyvanderHoe95])
and Justified Knowledge~$J$~\cite{Art06TCS}.
Justified Common Knowledge, introduced by Artemov~\cite{Art06TCS}, is a more general approach to the concept of common knowledge
which has been shown to have better proof-theoretic and complexity behavior.
The notion of justified knowledge grew from the studies of the Logic of Proofs~\cite{Art01BSL}.
The discovery of the justified common knowledge~$J$ brought under consideration
a whole variety of common knowledge operators for a given set of agents.
Here we introduce the logic~$\mathbf{S4}_n^{CJ}$,
which is formalized as a normal modal logic of $n$~agents
each represented by an $\mathbf{S4}$~modality~$K_i$ for $i = 1, 2, \ldots, n$.
The two types of common knowledge are also $\mathbf{S4}$~modalities and
satisfy the connection axiom for all~$i$ : $J\varphi \to K_i\varphi$ and $C\varphi \to K_i\varphi$.
In addition, there is an induction axiom for~$C$ alone:
$[\varphi \land C(\varphi \to E\varphi)] \to C\varphi$.
In~$\mathbf{S4}_n^{CJ}$ the modality~$C$ is the conventional common knowledge operator
whereas $J$~represents any common knowledge operator.
In particular, $J\varphi \to C\varphi$ is provable,
hence $C$~is provably the weakest of common knowledge operators.
We show that $\mathbf{S4}_n^{CJ}$~is sound and complete for a class of epistemic Kripke models.
As a result, we also have that $\mathbf{S4}_n^{CJ}$~has the finite model property and is decidable.
$\mathbf{S4}_n^{CJ}$~is conservative over both~$\mathbf{S4}_n^{C}$ and~$\mathbf{S4}_n^{J}$,
the analogous systems with a single common knowledge modality, $C$~or $J$ respectively.
This then offers a convenient testbed for analyzing different approaches to the common knowledge phenomenon
(cf.~\cite{Ant06TR}).}
}
@incollection{Ant07LFCS,
author = {Evangelia Antonakos},
title = {Justified and Common Knowledge: Limited Conservativity},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2007,
{N}ew {Y}ork, {NY}, {USA}, {J}une~4--7, 2007, Proceedings},
year = {2007},
editor = {Sergei N. Artemov and Anil Nerode},
volume = {4514},
series = {Lecture Notes in Computer Science},
pages = {1--11},
publisher = {Springer},
doi = {10.1007/978-3-540-72734-7_1},
conference = {http://lfcs.info/lfcs07/},
keywords = {justified knowledge, common knowledge, Artemov, conservative},
abstract = {We consider the relative strengths of three formal approaches to public knowledge:
``any fool'' knowledge by McCarthy~(1970), Common Knowledge by Halpern and Moses~(1990), and
Justified Knowledge by Artemov~(2004).
Specifically, we show that epistemic systems with the Common Knowledge modality~$C$ are
conservative with respect to Justified Knowledge systems on formulas $\chi \land C\varphi \to \psi$,
where $\chi$, $\varphi$, and $\psi$ are $C$-free.}
}
@inproceedings{ArlKis09FEW,
author = {Horacio Arl{\'{o}}-Costa and Kohei Kishida},
title = {Three Proofs and the {K}nower in the {Q}uantified {L}ogic of {P}roofs},
booktitle = {Online Proceedings of Sixth Annual {F}ormal {E}pistemology {W}orkshop ({FEW~2009})},
year = {2009},
address = {Carnegie Mellon University, Pittsburg, PA, USA},
month = jun # { 18--21,},
note = {Comments to~\cite{DeaKur09FEW}},
conference = {http://fitelson.org/few/few_09/},
pdf = {http://fitelson.org/few/few_09/hac_kk_comments.pdf},
abstract = {The Knower Paradox demonstrates that any theory~T which
1)~extends Robinson arithmetic~Q,
2)~includes a predicate~K(x) intended to formalize
the formula with Godel number~x is known by agent~i, and
3)~contains certain elementary epistemic principles involving~K(x) is inconsistent.
In~\cite{DeaKur09FEW} Dean and Kurokawa show that
the Knower can be proved in the Quantified Logic of Proofs~(QLP) formulated by Mel Fitting in~\cite{Fit08APAL} --
extending work presented by Artemov in~\cite{Art01BSL}.
Dean and Kurokawa argue that QLP~is more expressive than most modal logics and
that this permits to identify more clearly the epistemic principles used in the proof of the Knower.
They also argue that the proof seems to require the use of a suspect principle --
the Uniform Barcan Formula~(UBF).
So, they propose to resolve the paradox by abandoning~UBF.
In this note we offer three independent proofs of the Knower in~QLP
that do not require the use of~UBF.
So, it seems that the resolution of the paradox proposed by Dean and Kurokawa is not a viable option.
We conclude with some observations about possible resolutions of the paradox compatible with our results.}
}
@article{Art94APAL,
author = {Sergei [N.] Art{\"{e}}mov},
title = {Logic of proofs},
journal = {Annals of Pure and Applied Logic},
year = {1994},
volume = {67},
number = {1--3},
pages = {29--59},
month = may,
doi = {10.1016/0168-0072(94)90007-8},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/APAL94.ps},
review = {http://www.ams.org/mathscinet/pdf/1274284.pdf},
abstract = {In this paper individual proofs are integrated into provability logic.
Systems of axioms for a logic with operators ``$A$~is provable'' and ``$p$~is a proof of~$A$'' are introduced,
provided with Kripke semantics and decision procedure.
Completeness theorems with respect to the arithmetical interpretation are proved.}
}
@techreport{Art95TR,
author = {Sergei N. Artemov},
title = {Operational modal logic},
institution = {Cornell University},
year = {1995},
number = {MSI 95--29},
month = dec,
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/MSI95-29.ps},
abstract = {Answers to two old questions are given in this paper.\\
1. Modal logic~$\mathcal{S}4$, which was informally specified by G{\"{o}}del in~1933
as a logic for provability, meets its exact provability interpretation.\\
2. Brouwer - Heyting - Kolmogorov realizing operations~(1931-32) for intuitionistic logic~$\mathcal{Int}$
also get exact interpretation as corresponding propositional operations on proofs;
both~$\mathcal{S}4$ and~$\mathcal{Int}$ turn out to be complete with respect to this proof realization.
These results are based on operational reading of~$\mathcal{S}4$, where a modality is split into three operations.
The \emph{logic of proofs} with these operations is shown to be arithmetically complete
with respect to the intended provability semantics and sufficient to realize every operation on proofs
admitting propositional specification in arithmetic.}
}
@techreport{Art96TR,
author = {Sergei N. Artemov},
title = {Proof Realization of Intuitionistic and Modal Logics},
institution = {Cornell University},
year = {1996},
number = {MSI 96--06},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/MSI96-06.ps},
abstract = {Logic of Proofs~($\mathcal{LP}$) has been introduced in~\cite{Art95TR}
as a collection of all valid formulas in the propositional language with labeled logical connectives~$[[t]](\cdot)$
where $t$~is a \emph{proof term} with the intended reading of~$[[t]]F$ as ``$t$~\emph{is a proof of}~$F$''.
$\mathcal{LP}$ is supplied with a natural axiom system, completeness and decidability theorems.
$\mathcal{LP}$ may express some constructions of logic
which have been formulated or/and interpreted in an informal metalanguage involving the notion of proof,
e.g. the intuitionistic logic and its Brauwer-Heyting-Kolmogorov semantics,
classical modal logic~$\mathcal{S}4$, \emph{etc} (cf.~\cite{Art95TR}).
In the current paper we demonstrate how the intuitionistic propositional logic~$\mathcal{Int}$ can be
directily realized into the Logic of Proofs.
It is shown, that the proof realizability gives a fair semantics for~$\mathcal{Int}$.}
}
@techreport{Art97TRa,
author = {Sergei N. Artemov},
title = {Proof realizations of typed {$\lambda$}-calculi},
institution = {Cornell University},
year = {1997},
number = {MSI 97--02},
month = may,
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/MSI97-02.ps},
abstract = {The Logic of Proofs~($\mathcal{LP}$) introduced in~\cite{Art95TR} provides a basic framework for the formalization of reasoning about proofs.
It incorporates proof terms into the propositional language, using labeled logical operators~``$t : $''
with the intended reading of~$t:F$ being ``$t$~\emph{is a proof of}~$F$''.
$\mathcal{LP}$ is supplied with an exact provability semantics in Peano Arithmetic, a simple axiom system, and completeness and decidability theorems.
$\mathcal{LP}$ naturally expresses a number of constructions of logic involving the notion of proof, which have previously been formulated and/or interpreted in an informal metalanguage,
e.g. modal logic, Intuitionistic logic with its Brouwer-Heyting-Kolmogorov semantics, etc.~(\cite{Art95TR}, \cite{Art96TR}).
In the current paper we demonstrate how the typed $\lambda$-calculus and the modal $\lambda$-calculus can be realized in the Logic of Proofs.}
}
@techreport{Art97TRb,
author = {Sergei N. Artemov},
title = {On Proof Realization of Intuitionistic Logic},
institution = {Cornell University},
year = {1997},
number = {CFIS 97--08},
month = oct,
note = {Later version published as \cite{Art99JANCL}},
abstract = {In~1933 G{\"{o}}del introduced an axiomatic system, currently known as~S4, for a logic of an absolute provability,
i.e. not depending on the formalism chosen~([Goed33]).
The problem of finding a fair provability model for~S4 was left open.
The famous formal provability predicate which first appeared in the G{\"{o}}del Incompleteness Theorem does not do this job:
the logic of formal provability is not compatible with~S4.
As was discovered in~\cite{Art95TR}, this defect of the formal provability predicate can be bypassed
by replacing hidden quantifiers over proofs by \emph{proof polynomials} in a certain finite basis.
The resulting \emph{Logic of Proofs} enjoys a natural arithmetical semantics and provides an intended provability model for~S4,
thus answering a question left open by G{\"{o}}del in~1933.
Proof polynomials give an intended semantics for some other constructions based on the concept of provability,
including intuitionistic logic with its Brouwer-Heyting- Kolmogorov interpretation, $\lambda$-calculus and modal $\lambda$-calculus.
In the current paper we demonstrate how the intuitionistic propositional logic~$\mathcal{Int}$ can be directly realized by proof polynomials.
It is shown that $\mathcal{Int}$~is complete with respect to this proof realizability.}
}
@techreport{Art98TRa,
author = {Sergei N. Artemov},
title = {Logic of {P}roofs: a Unified Semantics for Modality and {$\lambda$}-terms},
institution = {Cornell University},
year = {1998},
number = {CFIS 98--06},
month = mar,
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CFIS98-06.ps},
abstract = {In~1933 G{\"{o}}del introduced a modal logic of provability~($\mathcal{S}4$) and left open the problem of a formal provability semantics for this logic.
We give a complete solution to this problem.
We find a sound and complete axiom system for the logic~($\mathcal{LP}$) with atomic propositions for explicit proofs ``$t$~\emph{is a proof of}~$F$'',
and construct an exact realization of~$\mathcal{S}4$ in~$\mathcal{LP}$ .
In~$\mathcal{LP}$ the reflection principle is valid, which circumvents some of the restrictions imposed on the provability operator by G{\"{o}}del's second incompleteness theorem.
$\mathcal{LP}$~formalizes the Kolmogorov calculus of problems and proves the Kolmogorov conjecture~(1932) that intuitionistic logic coincides with the classical calculus of problems.
$\mathcal{LP}$~has revealed the relationship between proofs and types, and subsumes the $\lambda$-calculus, modal $\lambda$-calculus and combinatory logic.}
}
@techreport{Art98TRb,
author = {Sergei N. Artemov},
title = {Explicit provability: the intended semantics for intuitionistic and modal logic},
institution = {Cornell University},
year = {1998},
number = {CFIS 98--10},
month = sep,
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CFIS98-10.ps},
abstract = {The intended meaning of intuitionistic logic is given by the Brouwer-Heyting-Kolmogorov~(\emph{BHK}) semantics
which informally defines intuitionistic truth as provability and specifies the intuitionistic connectives via operations on proofs.
The natural problem of formalizing the \emph{BHK} semantics and establishing the completeness of propositional intuitionistic logic~$\mathcal{Int}$
with respect to this semantics remained open until recently.
This question turned out to be a part of the more general problem of the intended semantics for G{\"{o}}del's modal logic of provability~$\mathcal{S}4$
with the atoms ``$F$~is provable'' which was open since~1933.
In this paper we present complete solutions to both of these problems.
We find the logic of explicit provability~($\mathcal{LP}$) with the atoms ``$t$~is a proof of~$F$'' and establish that every theorem of~$\mathcal{S}4$
admits a reading in~$\mathcal{LP}$ as the statement about explicit provability.
This provides the adequate provability semantics for~$\mathcal{S}4$ along the lines of a suggestion made by G{\"{o}}del in~1938.
The explicit provability reading of G{\"{o}}del's embedding of~$\mathcal{Int}$ into~$\mathcal{S}4$ gives the desired formalization of the \emph{BHK} semantics:
$\mathcal{Int}$ is shown to be complete with respect to this semantics.
In addition, $\mathcal{LP}$ has revealed the relationship between proofs and types, and subsumes the $\lambda$-calculus, modal $\lambda$-calculus and combinatory logic.}
}
@techreport{Art98TRc,
author = {Sergei N. Artemov},
title = {On explicit reflection in theorem proving and formal verification},
institution = {Cornell University},
year = {1998},
number = {CFIS 98--16},
month = dec,
note = {Later version published as \cite{Art99CADE}},
abstract = {The basic properties of soundness, extensibility, and stability required from a verification system~$\mathcal{V}$ taken in full
yield the necessity of having a reflection rule in every such~$\mathcal{V}$.
However, the reflection rule based on the G{\"{o}}del provability predicate (implicit provability predicate) leads to a ``reflection tower'' of theories which cannot be formally verified.
The paper introduces an explicit reflection mechanism which can be verified inside the system.
This circumvents the reflection tower and provides a strict justification for the verification process.
On the practical side, the paper gives specific recommendations concerning the verification of inference rules and building a verifiable reflection mechanism for a theorem proving system.}
}
@techreport{Art98TRd,
author = {Sergei N. Artemov},
title = {Explicit Modal Logic},
institution = {Cornell University},
year = {1998},
number = {CFIS 98--17},
month = dec,
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/Upp.ps},
note = {Extended version \cite{Art99TRa} later published as \cite{Art00AiML}},
abstract = {In~1933 G{\"{o}}del introduced a modal logic of provability~($\mathcal{S}4$) and left open the problem of a formal provability semantics for this logic.
Since then numerous attempts have been made to give an adequate provability semantics to G{\"{o}}del's provability logic with only partial success.
In this paper we give the complete solution to this problem in the Logic of Proofs~($\mathcal{LP}$).
$\mathcal{LP}$~implements G{\"{o}}del's suggestion~(1938) of replacing formulas ``$F$~is provable''
by the propositions for explicit proofs ``$t$~is a proof of~$F$''~($t:F$).
$\mathcal{LP}$~admits the reflection of explicit proofs $t:F \to F$ thus circumventing restrictions
imposed on the provability operator by G{\"{o}}del's second incompleteness theorem.
$\mathcal{LP}$~formalizes the Kolmogorov calculus of problems and proves the Kolmogorov conjecture that intuitionistic logic coincides with the classical calculus of problems.}
}
@techreport{Art99TRa,
author = {Sergei N. Artemov},
title = {Operations on proofs that can be specified by means of modal logic},
institution = {Cornell University},
year = {1999},
number = {CFIS 99--02},
month = feb,
note = {Later version published as \cite{Art00AiML}},
abstract = {Explicit modal logic was first sketched by G{\"{o}}del in~\cite{Goed38CW} as the logic with the atoms ``$t$~\emph{is a proof of}~$F$''.
The complete axiomatization of the Logic of Proofs~$\mathcal{LP}$ was found in~\cite{Art95TR} (see also~\cite{Art02CSLI},\cite{Art98TRb},\cite{JapdeJon98HPT}).
In this paper we establish a sort of a functional completeness property of \emph{proof polynomials} which constitute the system of proof terms in~$\mathcal{LP}$.
Proof polynomials are built from variables and constants by three operations on proofs: ``$\cdot$''~(application), ``$!$''~(proof checker), and ``$+$''~(choice).
Here constants stand for canonical proofs of ``simple facts'', namely instances of propositional axioms and axioms of~$\mathcal{LP}$ in a given proof system.
We show that every operation on proofs that (i)~can be specified in a propositional modal language and (ii)~is invariant with respect to the choice of a proof system is realized by a proof polynomial.}
}
@techreport{Art99TRb,
author = {Sergei N. Artemov},
title = {Deep isomorphism of modal derivations and {$\lambda$}-terms},
institution = {Cornell University},
year = {1999},
number = {CFIS 99--07},
month = jun,
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CFIS99-07.ps},
abstract = {The traditional Curry-Howard isomorphism given a derivation of~$F$ from assumptions~$\Gamma$ in intuitionistic modal logic constructs the $\lambda$-term~$t(\mathbf{x})$
such that the sequent $\mathbf{x}:\Gamma \Rightarrow t(\mathbf{x}):F$ is derivable in the corresponding calculus of typed modal $\lambda$-terms.
Technically speaking this isomorphism is a realization by $\lambda$-terms of the outermost modalities in some (not all) derivable modal sequents $[]\Gamma \Rightarrow []F$.
In this talk we describe a system of $\lambda$-terms (in the combinatory terms form)~$\mathbf{LPi}$ sufficient for a uniform realization of all modalities (not just the outermost ones)
in any derivable modal sequent.
The expressive power of~$\mathbf{LPi}$ surpasses the one of the usual modal $\lambda$-calculus.
$\mathbf{LPi}$~also extends the natural provability semantics of Curry-Howard terms under which $t:F$~can be interpreted as ``$t$~is a proof of~$F$ in a given sufficiently rich system,
e.g. Heyting Arithmetic $\mathbf{HA}$''.}
}
@incollection{Art99FLoC,
author = {Sergei N. Artemov},
title = {Uniform provability realization of intuitionistic logic, modality and {$\lambda$}-terms},
booktitle = {Tutorial Workshop on Realizability Semantics and Applications
(associated to {FLoC}'99, the 1999 {F}ederated {L}ogic {C}onference),
{T}rento, {I}taly, 30 {J}une--1 {J}uly 1999},
year = {1999},
editor = {Lars Birkedal and Jaap van Oosten and Giuseppe Rosolini and Dana S. Scott},
volume = {23(1)},
series = {Electronic Notes in Theoretical Computer Science},
pages = {3--12},
publisher = {Elsevier},
doi = {10.1016/S1571-0661(04)00100-8},
conference = {http://floc99.itc.it/conferences/w10/w10.htm},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CFIS99-08.ps},
abstract = {The intended meaning of intuitionistic logic is explained by the Brouwer-Heyting-Kolmogorov~(\emph{BHK}) provability semantics which informally defines intuitionistic truth
as provability and specifies the intuitionistic connectives via operations on proofs.
The problem of finding an adequate formalization of the provability semantics and establishing the completeness of the intuitionistic logic~$\mathbf{Int}$ was first raised by G{\"{o}}del in~1933.
This question turned out to be a part of the more general problem of the intended realization for G{\"{o}}del's modal logic of provability~$\mathbf{S4}$ which was open since~1933.
In this tutorial talk we present a provability realization of~$\mathbf{Int}$ and~$\mathbf{S4}$ that solves both of these problems.
We describe the logic of explicit provability~($\mathbf{LP}$) with the atoms ``$t$~is a proof of~$F$'' and establish that every theorem of~$\mathbf{S4}$ admits
a reading in~$\mathbf{LP}$ as the statement about operations on proofs.
Moreover, both~$\mathbf{S4}$ and~$\mathbf{Int}$ are shown to be complete with respect to this realization.
In addition, $\mathbf{LP}$~subsumes the $\lambda$-calculus, modal $\lambda$-calculus, combinatory logic and provides a uniform provability realization of modality and $\lambda$-terms.}
}
@incollection{Art99CADE,
author = {Sergei N. Artemov},
title = {On Explicit Reflection in Theorem Proving and Formal Verification},
booktitle = {Automated Deduction~--- {CADE}--16,
16th International {C}onference on {A}utomated {D}eduction,
{T}rento, {I}taly, {J}uly 7--10, 1999, Proceedings},
year = {1999},
editor = {Harald Ganzinger},
volume = {1632},
series = {Lecture Notes in Artificial Intelligence},
pages = {267--281},
publisher = {Springer},
doi = {10.1007/3-540-48660-7_23},
conference = {http://floc99.itc.it/conferences/cade/cade.htm},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CADE99.ps},
abstract = {We show that the stability requirement for a verification system yields the necessity of some sort of a reflection mechanism.
However, the traditional reflection rule based on the G{\"{o}}del implicit provability predicate leads to a ``reflection tower'' of theories which cannot be formally verified.
We found natural lower and upper bounds on a metatheory capable of establishing stability of a given verification system.
The paper also introduces an explicit reflection mechanism which can be verified internally.
This circumvents the reflection tower and provides a theoretical justification for the verification process.
On the practical side, the paper gives specific recommendations concerning verification of inference rules and building a verifiable reflection mechanism for a theorem proving system.}
}
@article{Art99JANCL,
author = {S[ergei] N. Artemov},
title = {Realization of Intuitionistic Logic by Proof Polynomials},
journal = {Journal of Applied Non-Classical Logics},
year = {1999},
volume = {9},
number = {2--3},
pages = {285--302},
jancl = {http://www.irit.fr/ACTIVITES/EQ_ALG/Jancl/Abstracts/abstract-9.2.html},
bl = {http://direct.bl.uk/research/12/20/RN068980215.html},
review = {http://www.ams.org/mathscinet/pdf/1825569.pdf},
abstract = {In~1933 G{\"{o}}del introduced an axiomatic system, currently known as~S4, for a logic of an absolute provability, i.e. not depending on the formalism chosen~[Goed33]).
The problem of finding a fair provability model for~S4 was left open.
The famous formal provability predicate which first appeared in the G{\"{o}}del Incompleteness Theorem does not do this job: the logic of formal provability is not compatible with~S4.
As was discovered in~\cite{Art95TR}, this defect of the formal provability predicate can be bypassed by replacing hidden quantifiers over proofs by \emph{proof polynomials} in a certain finite basis.
The resulting \emph{Logic of Proofs} enjoys a natural arithmetical semantics and provides an intended provability model for~S4, thus answering a question left open by G{\"{o}}del in~1933.
Proof polynomials give an intended semantics for some other constructions based on the concept of provability, including intuitionistic logic with its Brouwer-Heyting- Kolmogorov interpretation,
lambda-calculus and modal lambda-calculus.
In the current paper we demonstrate how the intuitionistic propositional logic~\emph{Int} can be directly realized by proof polynomials.
It is shown, that \emph{Int} is complete with respect to this proof realizability.}
}
@incollection{Art00AiML,
author = {Sergei N. Artemov},
title = {Operations on Proofs that can be Specified by Means of Modal Logic},
booktitle = {Advances in Modal Logic, volume 2},
year = {2000},
editor = {Michael Zakharyaschev and Krister Segerberg and Maarten de Rijke and Heinrich Wansing},
volume = {118},
pages = {77--90},
series = {{CSLI} Lecture Notes},
publisher = {CSLI Publications},
address = {Stanford},
conference = {http://www.aiml.net/conferences/aiml-1998/},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/AiML.ps},
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:01735872&type=pdf&format=complete},
pubweb = {http://cslipublications.stanford.edu/site/1575862727.shtml},
distrweb = {http://www.press.uchicago.edu/presssite/metadata.epl?mode=synopsis&bookkey=36229},
abstract = {Explicit modal logic was first sketched by G{\"{o}}del in~\cite{Goed38CW} as the logic with the atoms ``$t$~\emph{is a proof of}~$F$''.
The complete axiomatization of the Logic of Proofs~$\mathcal{LP}$ was found in~\cite{Art95TR} (see also~\cite{Art02CSLI},\cite{Art98TRb},\cite{JapdeJon98HPT}).
In this paper we establish a sort of a functional completeness property of \emph{proof polynomials} which constitute the system of proof terms in~$\mathcal{LP}$.
Proof polynomials are built from variables and constants by three operations on proofs: ``$\cdot$''~(application), ``$!$''~(proof checker), and ``$+$''~(choice).
Here constants stand for canonical proofs of ``simple facts'', namely instances of propositional axioms and axioms of~$\mathcal{LP}$ in a given proof system.
We show that every operation on proofs that (i)~can be specified in a propositional modal language and (ii)~is invariant with respect to the choice of a proof system is realized by a proof polynomial.}
}
@article{Art01BSL,
author = {Sergei N. Artemov},
title = {Explicit Provability and Constructive Semantics},
journal = {Bulletin of Symbolic Logic},
year = {2001},
volume = {7},
number = {1},
pages = {1--36},
month = mar,
euclid = {http://projecteuclid.org/euclid.bsl/1182353754},
jstor = {http://www.jstor.org/stable/2687821},
ps = {http://www.math.ucla.edu/~asl/bsl/0701/0701-001.ps},
review = {http://www.ams.org/mathscinet/pdf/1836474.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:01623806&type=pdf&format=complete},
abstract = {In~1933 G{\"{o}}del introduced a calculus of provability (also known as modal logic~$\mathbf{S4}$) and left open the question of its exact intended semantics.
In this paper we give a solution to this problem.
We find the logic~$\mathbf{LP}$ of propositions and proofs and
show that G{\"{o}}del's provability calculus is nothing but the forgetful projectiof of~$\mathbf{LP}$.
This also achieves G{\"{o}}del's objective of defining intuitionistic propositional logic~$\mathbf{Int}$
via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for~$\mathbf{Int}$
which resisted formalization since early~1930s.
$\mathbf{LP}$ may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and $\lambda$-calculus.}
}
@inproceedings{Art02LC,
author = {Sergei [N.] Artemov},
title = {Incompleteness theorem and two models for provability},
booktitle = {2001~{E}uropean Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'01,
{V}ienna, {A}ustria, {A}gust 6--11, 2001},
year = {2002},
volume = {8(1)},
series = {Bulletin of Symbolic Logic},
pages = {120},
month = mar,
publisher = {Association for Symbolic Logic},
note = {Abstract of invited talk},
ps = {http://www.math.ucla.edu/~asl/bsl/0801/0801-006.ps},
doi = {10.2178/bsl/1182353864},
jstor = {http://www.jstor.org/stable/2687746},
abstract = {G{\"{o}}del's Incompleteness theorem and his papers of~1933 and~1938 led to two essentially different models for provability,
each having its own areas of applications.
A.~Loeb's modal logic~L of formal provability (also known as~GL, G, PRL, K4.W)
where the ``non-reflexive'' Loeb principle is present.
Within this model proofs are represented implicitly by existential quantifiers.
The highlights of this model are the propositional formalization of the Second Incompleteness Theorem and Loeb's theorem,
De~Jongh-Sambin fixed point theorem, and the Solovay completeness theorem.
The logic~L finds applications in traditional proof theory.
B.~G{\"{o}}del's modal logic for provability (also known as~S4) and its counterpart logic of proofs~LP
with the reflection principle ``provable~$F$ implies~$F$''.
Within his model proofs are represented explicitly by combinatory style terms.
This model has reached out to such areas as constructive semantics, logics of knowledge, combinatory logic and lambda-calculus,
automated deduction and formal verification, and typed programming languages.
The models~A and~B are compatible because they are both based on the same G{\"{o}}del provability predicate.}
}
@incollection{Art02CSLI,
author = {Sergei N. Artemov},
title = {Unified Semantics for Modality and {$\lambda$}-terms via Proof Polynomials},
booktitle = {Algebras, Diagrams and Decisions in Language, Logic and Computation},
publisher = {{CSLI} {P}ublications},
year = {2002},
editor = {Kees Vermeulen and Ann Copestake},
series = {CSLI Lecture Notes},
address = {Stanford},
volume = {144},
pages = {89--118},
pubweb = {http://cslipublications.stanford.edu/site/1575863723.shtml},
distrweb = {http://www.press.uchicago.edu/presssite/metadata.epl?mode=synopsis&bookkey=28673},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CSLI.ps},
abstract = {It is shown that the modal logic~$\mathcal{S}4$, simple $\lambda$-calculus and modal $\lambda$-calculus admit a realization
in a very simple propositional logical system~$\mathcal{LP}$,
which has an exact provability semantics.
In~$\mathcal{LP}$ both modality and $\lambda$-terms become objects of the same nature,
namely, proof polynomials.
The provability interpretation of modal $\lambda$-terms presented here may be regarded as a systemindependent generalization of the Curry-Howard isomorphism of proofs and $\lambda$-terms.}
}
@inproceedings{Art03DLC,
author = {Sergei [N.] Artemov},
title = {From Proof Polynomials to Reflexive Combinators},
booktitle = {Second {St.~P}etersburg Conference on Days of Logic and Computability},
year = {2003},
month = aug # { 24--26,},
address = {{St.~P}etersburg, {R}ussia},
note = {Abstract},
conference = {http://logic.pdmi.ras.ru/2ndDays/index.html},
abstract = {http://atlas-conferences.com/cgi-bin/abstract/cajy-40}
}
@incollection{Art03CSL,
author = {Sergei [N.] Artemov},
title = {Back to the Future: Explicit Logic for Computer Science},
booktitle = {Computer {S}cience {L}ogic,
17th~International Workshop {CSL}~2003,
12th~Annual Conference of the {EACSL},
8th~{K}urt {G\"{o}}del {C}olloquium, {KGC}~2003,
{V}ienna, {A}ustria, {A}ugust 25--30, 2003, Proceedings},
publisher = {Springer},
year = {2003},
editor = {Matthias Baaz and Johann A. Makowsky},
volume = {2803},
series = {Lecture Notes in Computer Science},
pages = {43},
note = {Abstract of invited lecture},
doi = {10.1007/b13224},
pdf = {http://springerlink.metapress.com/content/ha254l07p0lqayj9/fulltext.pdf?page=1},
conference = {http://www.logic.at/csl03/},
slides = {http://web.cs.gc.cuny.edu/~sartemov/publications/CLS03.pdf},
abstract = {We will speak about three traditions in Logic:
-~\emph{Classical}, usually associated with Frege, Hilbert, G{\"{o}}del, Tarski, and others;
-~\emph{Intuitionistic}, founded by Brouwer, Heyting, Kolmogorov, G{\"{o}}del, Kleene, and others;
-~\emph{Explicit}, which we trace back to Skolem, Curry, G{\"{o}}del, Church, and others.
The classical tradition in logic based on quantifiers~$\forall$ and~$\exists$ essentially reflected the 19th~century mathematician's way of representing dependencies between entities.
A sentence~$\forall x\exists yA(x,y)$,
though specifying a certain relation between~$x$ and~$y$,
did not mean that the latter is a function of the former,
let alone a computable one.
The Intuitionistic approach provided a principal shift toward the effective functional reading of the mathematician's quantifiers.
A new, non-Tarskian semantics had been suggested by Kleene:
realizability that revealed a computational content of logical derivations.
In a decent intuitionstic system,
a proof of~$\forall x\exists yA(x,y)$ yields a program~$f$ that computes $y=f(x)$.
Explicit tradition makes the ultimate step by using representative systems of functions instead of quantifiers from the very beginning.
Since the work of Skolem,~1920, it has been known that the classical logic can be adequately recast in this way.
Church in~1936 showed that even the very basic system of function definition and function application is capable of emulating any computable procedure.
However, despite this impressive start, the explicit tradition remained a Cinderella of the mathematical logic for decades.
Now things have changed: due to its very explicitness, this third tradition became the one most closely connected with Computer Science.
In this talk we will show how switching from quantifiers to explicit functional language helps problem solving in both theoretical logic and its applications.
A discovery of a natural system of self-referential proof terms, \emph{proof polynomials}, was essential in the solution to an open problem of G{\"{o}}del concerning formalization of provability.
Proof polynomials considerably extend the Curry-Howard isomorphism and lead to a joint calculus of propositions and proofs which unifies several previously unrelated areas.
It changes our conception of the appropriate syntax and semantics for reasoning about knowledge, functional programming languages, formalized deduction and verification.}
}
@article{Art03PSIM,
author = {S[ergei] N. Artemov},
title = {Embedding of the Modal {$\lambda$}-Calculus into the {L}ogic of {P}roofs},
journal = {Proceedings of the Steklov Institute of Mathematics},
year = {2003},
volume = {242},
number = {3},
pages = {36--49},
note = {Originally published in Russian},
mathnet = {http://mi.mathnet.ru/eng/tm404},
russian = {http://www.cs.gc.cuny.edu/~sartemov/publications/TSIM044.PS},
abstract = {The Logic of Proofs~\textbf{LP} introduced by the author may be regarded as a basic formal system for reasoning about propositions and proofs.
\textbf{LP}~comes from G{\"{o}}del's calculus of provability, also known as modal logic~\textbf{S4} to which P.~S.~Novikov devoted the well-known monograph \textit{Constructive Mathematical Logic from the Point of View of the Classical One}.
\textbf{LP}~gives an exact mathematical answer to the question of the provability semantics of~\textbf{S4} raised by G{\"{o}}del.
This paper gives a comparison of the expressive powers of~\textbf{LP}, the typed $\lambda$-calculus, and the modal $\lambda$-calculus.
It is shown that a small (namely, Horn) fragment of~\textbf{LP} is sufficient for a natural embedding of the typed $\lambda$-calculus.
It is also shown that \textbf{LP}~models the modal $\lambda$-calculus.}
}
@techreport{Art04TR,
author = {Sergei [N.] Artemov},
title = {Evidence-Based Common Knowledge},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2004},
number = {TR--2004018},
month = nov,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=140},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004018.pdf},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2004018.ps},
note = {Revised in April 2005; later published as~\cite{Art06TCS}},
abstract = {In this paper we introduce a new type of knowledge operator, called \emph{evidence-based knowledge}, intended to capture the constructive core of common knowledge.
An evidence-based knowledge system is obtained by augmenting a multi-agent logic of knowledge
with a system of evidence assertions~$t:\varphi$ (``$t$~is an evidence for~$\varphi$'')
based on the following plausible assumptions: 1)~each axiom has evidence; 3)~evidence is checkable; 3)~any evidence implies individual knowledge for each agent.
Normally, the following monotonicity property is also assumed: 4)~any piece of evidence is compatible with any other evidence.
We show that the evidence-based knowledge operator is a stronger version of the common knowledge operator.
Evidence-based knowledge is free of logical omniscience, model-independent, and has natural motivation.
Furthermore, evidence-based knowledge can be presented by normal multi-modal logics,
which are in the scope of well-developed machinery applicable to modal logic:
epistemic models, normalized proofs, automated proof search, etc.}
}
@article{Art04RMS,
author = {S[ergei] N. Artemov},
title = {{K}olmogorov and {G\"{o}}del's approach to intuitionistic logic: current developments},
journal = {Russian Mathematical Surveys},
year = {2004},
volume = {59},
number = {2},
pages = {203--229},
note = {Originally published in Russian},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/RusMatSurveys.ps},
doi = {10.1070/RM2004v059n02ABEH000715},
mathnet = {http://mi.mathnet.ru/eng/umn715},
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:02120744&type=pdf&format=complete},
abstract = {Intuitionistic mathematics was created by Brouwer on the basis of constructive reasoning,
where the existence of a proof was the criterion for truth.
Kolmogorov and G{\"{o}}del proposed interpreting intuitionistic logic on the basis of classical notions
of a problem's solution and of provability.
In~1933 G{\"{o}}del made the first substantial step toward the building of such an interpretation.
Despite much progress in the understanding of intuitionism,
this task was not complete before the author's 1995~paper~\cite{Art95TR}.
This survey will cover the results of the past decade obtained within this framework.}
}
@incollection{Art05Gabbay,
author = {Sergei [N.] Artemov},
title = {Existential Semantics for Modal Logic},
booktitle = {We Will Show Them! {E}ssays in Honour of {D}ov {G}abbay},
publisher = {College Publications},
year = {2005},
editor = {Sergei [N.] Artemov and Howard Barringer and d'Avila Garcez, Artur S. and Lu{\'{\i}}s C. Lamb and John Woods},
volume = {1},
pages = {19--30},
pubweb = {http://www.collegepublications.co.uk/tributes/?00002}
}
@article{Art06TCS,
author = {Sergei [N.] Artemov},
title = {Justified common knowledge},
journal = {Theoretical Computer Science},
year = {2006},
volume = {357},
number = {1--3},
pages = {4--22},
month = jul,
doi = {10.1016/j.tcs.2006.03.009},
review = {http://www.ams.org/mathscinet/pdf/2242754.pdf},
keywords = {epistemic logic, common knowledge, justification, logic of proofs},
abstract = {In this paper we introduce the \emph{justified knowledge} operator~$J$ with the intended meaning of~$J\varphi$
as `there is a justification for~$\varphi$.'
Though justified knowledge appears here in a case study of common knowledge systems,
a similar approach is applicable in more general situations.
First we consider \emph{evidence-based common knowledge} systems obtained by augmenting a multi-agent logic
of knowledge with a system of evidence assertions~$t:\varphi$, reflecting the notion
`$t$~is an evidence for~$\varphi$,' such that evidence is respected by all agents.
\emph{Justified common knowledge} is obtained by collapsing all evidence terms into one modality~$J$.
We show that in standard situations, when the base epistemic systems are~$\mathsf{T}$, $\mathsf{S4}$, and~$\mathsf{S5}$,
the resulting justified common knowledge systems are normal modal logics,
which places them within the scope of well-developed machinery applicable to modal logic:
Kripke-style epistemic models, normalized proofs, automated proof search, etc.
In the aforementioned situations, the intended semantics of justified knowledge is supported by a realization theorem stating that
for any valid fact about justified knowledge, one could recover its constructive meaning
by realizing all occurrences of justified knowledge modalities~$J\varphi$
by appropriate evidence terms~$t:\varphi$.}
}
@incollection{Art07IMS,
author = {Sergei [N.] Artemov},
title = {On Two Models of Provability},
booktitle = {Mathematical Problems from Applied Logic {II}, Logics for the {XXI}st Century},
publisher = {Springer},
year = {2007},
editor = {Dov M. Gabbay and Sergei S. Goncharov and Michael Zakharyaschev},
volume = {5},
series = {International Mathematical Series},
pages = {1--52},
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:05168265&type=pdf&format=complete},
doi = {10.1007/978-0-387-69245-6_1}
}
@techreport{Art07TRa,
author = {Sergei [N.] Artemov},
title = {Symmetric {L}ogic of {P}roofs},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007016},
month = sep,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=340},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007016.pdf},
note = {Later version published as~\cite{Art08LNCS}},
abstract = {The Logic of Proofs~$\mathsf{LP}$ captures the invariant propositional properties of proof predicates
$t$~\emph{is a proof of}~$F$ with a set of operations on proofs sufficient for realizing the whole modal logic~$\mathsf{S4}$
and hence the intuitionistic logic~$\mathsf{IPC}$.
Some intuitive properties of proofs, however, are not invariant and hence not present in~$\mathsf{LP}$.
For example, the choice function~`$+$' in~$\mathsf{LP}$,
which is specified by the condition $s:F \lor t:F \to (s+t):F$, is not necessarily symmetric.
In this paper, we introduce an extension of the Logic of Proofs,~$\mathsf{SLP}$,
which incorporates natural properties of the standard proof predicate in Peano Arithmetic:
\[
\textit{$t$~is a code of a derivation containing~$F$,}
\]
including the symmetry of Choice.
We show that $\mathsf{SLP}$~produces Brouwer-Heyting-Kolmogorov proofs with a rich structure,
which can be useful for applications in epistemic logic and other areas.}
}
@techreport{Art07TRb,
author = {Sergei [N.] Artemov},
title = {Justification Logic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007019},
month = oct,
note = {Extended version~\cite{Art08TRa} later published as~\cite{Art08RSL}},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=343},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007019.pdf},
abstract = {We describe a general logical framework, Justification Logic, for reasoning about epistemic justification.
Justification Logic is based on classical propositional logic augmented by justification assertions~$t:F$
that read $t$~\emph{is a justification for}~$F$.
Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs.
It contributes to the studies of the well-known \emph{Justified True Belief vs.~Knowledge} problem.
As a case study, we formalize Gettier examples in Justification Logic and reveal hidden assumptions and redundancies in Gettier reasoning.
We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a robust system of justifications.
This renders a new, evidence-based foundation for epistemic logic.}
}
@incollection{Art07MLH,
author = {Sergei [N.] Artemov},
title = {Modal logic in mathematics},
booktitle = {Handbook of Modal Logic},
publisher = {Elsevier},
year = {2007},
editor = {Patrick Blackburn and van Benthem, Johan and Frank Wolter},
volume = {3},
series = {Studies in Logic and Practical Reasoning},
chapter = {16},
pages = {927--969},
doi = {10.1016/S1570-2464(07)80019-X}
}
@incollection{Art08LNCS,
author = {Sergei [N.] Artemov},
title = {Symmetric {L}ogic of {P}roofs},
booktitle = {Pillars of Computer Science, Essays Dedicated to {B}oris ({B}oaz) {T}rakhtenbrot on the Occasion of His 85th Birthday},
publisher = {Springer},
year = {2008},
editor = {Arnon Avron and Nachum Dershowitz and Alexander Rabinovich},
volume = {4800},
series = {Lecture Notes in Computer Science},
pages = {58--71},
doi = {10.1007/978-3-540-78127-1_4},
abstract = {The Logic of Proofs~$\mathsf{LP}$ captures the invariant propositional properties of proof predicates
$t$~\emph{is a proof of}~$F$ with a set of operations on proofs sufficient for realizing the whole modal logic~$\mathsf{S4}$
and hence the intuitionistic logic~$\mathsf{IPC}$.
Some intuitive properties of proofs, however, are not invariant and hence not present in~$\mathsf{LP}$.
For example, the choice function~`$+$' in~$\mathsf{LP}$,
which is specified by the condition $s:F \lor t:F \to (s+t):F$, is not necessarily symmetric.
In this paper, we introduce an extension of the Logic of Proofs,~$\mathsf{SLP}$,
which incorporates natural properties of the standard proof predicate in Peano Arithmetic:
\[
\textit{$t$~is a code of a derivation containing~$F$,}
\]
including the symmetry of Choice.
We show that $\mathsf{SLP}$~produces Brouwer-Heyting-Kolmogorov proofs with a rich structure,
which can be useful for applications in epistemic logic and other areas.}
}
@techreport{Art08TRa,
author = {Sergei [N.] Artemov},
title = {The Logic of Justification},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2008},
number = {TR--2008010},
month = sep,
note = {Later version published as \cite{Art08RSL}},
http = {http://tr.cs.gc.cuny.edu/tr/techreport.php?id=359},
pdf = {http://tr.cs.gc.cuny.edu/tr/files/TR-2008010.pdf},
abstract = {We describe a general logical framework, Justification Logic, for reasoning about epistemic justification.
Justification Logic is based on classical propositional logic augmented by justification assertions~$t:F$
that read $t$~\emph{is a justification for}~$F$.
Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs.
It contributes to the studies of the well-known \emph{Justified True Belief vs.~Knowledge} problem.
We state a general Correspondence Theorem showing that behind each epistemic modal logic,
there is a robust system of justifications.
This renders a new, evidence-based foundation for epistemic logic.
As a case study, we offer a resolution of the Goldman-Kripke `Red Barn' paradox and
analyze Russell's `prime minister example' in Justification Logic.
Furthermore, we formalize the well-known Gettier example and reveal hidden assumptions and
redundancies in Gettier's reasoning.}
}
@techreport{Art08TRb,
author = {Sergei [N.] Artemov},
title = {Why Do We Need {J}ustification {L}ogic?},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2008},
number = {TR--2008014},
month = sep,
http = {http://tr.cs.gc.cuny.edu/tr/techreport.php?id=366},
pdf = {http://tr.cs.gc.cuny.edu/tr/files/TR-2008014.pdf},
abstract = {In this paper, we will sketch the basic system of Justification Logic,
which is a general logical framework for reasoning about epistemic justification.
Justification Logic renders a new, evidence-based foundation for epistemic logic.
As a case study, we compare formalizations of the Kripke `Red Barn' scenario in modal epistemic logic and Justification Logic and
show here that the latter provides a deeper analysis.
In particular, we argue that modal language fails to fully represent the epistemic closure principle
whereas Justification Logic provides its adequate formalization.}
}
@incollection{Art08JELIA,
author = {Sergei [N.] Artemov},
title = {Justification {L}ogic},
booktitle = {Logics in Artificial Intelligence, 11th European Conference, {JELIA} 2008,
{D}resden, {G}ermany, {S}eptember 28 - {O}ctober 1, 2008, Proceedings},
publisher = {Springer},
year = {2008},
editor = {Steffen H{\"{o}}lldobler and Carsten Lutz and Heinrich Wansing},
volume = {5293},
series = {Lecture Notes in Artificial Intelligence},
pages = {1--4},
doi = {10.1007/978-3-540-87803-2_1},
conference = {http://www.jelia.eu/2008/}
}
@article{Art08RSL,
author = {Sergei [N.] Artemov},
title = {The Logic of Justification},
journal = {The Review of Symbolic Logic},
year = {2008},
volume = {1},
number = {4},
pages = {477--513},
month = dec,
doi = {10.1017/S1755020308090060},
abstract = {We describe a general logical framework, Justification Logic, for reasoning about epistemic justification.
Justification Logic is based on classical propositional logic augmented by justification assertions~$t:F$
that read $t$~\emph{is a justification for}~$F$.
Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs.
It contributes to the studies of the well-known \emph{Justified True Belief vs.~Knowledge} problem.
We state a general Correspondence Theorem showing that behind each epistemic modal logic,
there is a robust system of justifications.
This renders a new, evidence-based foundation for epistemic logic.
As a case study, we offer a resolution of the Goldman-Kripke `Red Barn' paradox and
analyze Russell's `prime minister example' in Justification Logic.
Furthermore, we formalize the well-known Gettier example and reveal hidden assumptions and
redundancies in Gettier's reasoning.}
}
@techreport{Art10TR,
author = {Sergei [N.] Artemov},
title = {Tracking Evidence},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2010},
number = {TR--2010004},
month = apr,
note = {Later version published as \cite{Art10LNCS}},
http = {http://tr.cs.gc.cuny.edu/tr/techreport.php?id=391},
pdf = {http://tr.cs.gc.cuny.edu/tr/files/TR-2010004.pdf},
abstract = {In this case study we describe an approach to a general logical framework for tracking evidence within epistemic contexts.
We consider as basic an example which features two justifications for a true statement,
one which is correct and one which is not.
We formalize this example in a system of Justification Logic with two knowers:
the object agent and the observer,
and we show that whereas the object agent does not logically distinguish between factive and non-factive justifications,
such distinctions can be attained at the observer level by analyzing the structure of evidence terms.
Basic logic properties of the corresponding two-agent Justification Logic system have been established,
which include Kripke-Fitting completeness.
We also argue that a similar evidence-tracking approach can be applied to analyzing paraconsistent systems.}
}
@incollection{Art10LNCS,
author = {Sergei [N.] Artemov},
title = {Tracking Evidence},
booktitle = {Fields of Logic and Computation, Essays Dedicated to {Y}uri {G}urevich on the Occasion of His 70th Birthday},
publisher = {Springer},
year = {2010},
editor = {Andreas Blass and Nachum Dershowitz and Wolfgang Reisig},
volume = {6300},
series = {Lecture Notes in Computer Science},
pages = {61--74},
doi = {10.1007/978-3-642-15025-8_3},
keywords = {justification, epistemic logic, evidence},
abstract = {In this case study we describe an approach to a general logical framework for tracking evidence within epistemic contexts.
We consider as basic an example which features two justifications for a true statement,
one which is correct and one which is not.
We formalize this example in a system of Justification Logic with two knowers:
the object agent and the observer,
and we show that whereas the object agent does not logically distinguish between factive and non-factive justifications,
such distinctions can be attained at the observer level by analyzing the structure of evidence terms.
Basic logic properties of the corresponding two-agent Justification Logic system have been established,
which include Kripke-Fitting completeness.
We also argue that a similar evidence-tracking approach can be applied to analyzing paraconsistent systems.}
}
@incollection{Art10LogKCA,
author = {Sergei [N.] Artemov},
title = {Justification of Knowledge: Philosophy and Logic},
booktitle = {{LogKCA-10}, Proceedings of the Second {ILCLI} International Workshop on Logic and Philosophy of Knowledge, Communication and Action},
publisher = {University of the Basque Country Press},
year = {2010},
editor = {Xabier Arrazola and Mar{\'{\i}}a Ponte},
pages = {17--36},
conference = {http://www.ilcli.ehu.es/p287-content/en/contenidos/informacion/ilcli_conferences/en_confe/conferences.html},
abstract = {Of Plato's tripartite analysis of knowledge,
\emph{justified true belief},
the traditional modal approach to epistemology leaves justification out of the picture.
Justification Logic augments epistemic logic by assertions~$t:F$ that read
\begin{center}
\emph{$t$~is a justification for~$F$}
\end{center}
hence incorporating all three of Plato's criteria.
Justification Logic absorbs basic principles that originate from both mainstream epistemology and the mathematical theory of proofs.
A general Correspondence Theorem shows that behind each epistemic modal logic lies a robust system of justifications.
This renders an evidence-based foundation for formal epistemology.}
}
@techreport{ArtBek04PR,
author = {Sergei N. Artemov and Lev D. Beklemishev},
title = {Provability Logic},
institution = {{L}ogic {G}roup {P}reprint {S}eries, {D}epartment of {P}hilosophy, {U}trecht {U}niversity},
year = {2004},
type = {Preprint},
number = {234},
month = nov,
note = {Later version published as~\cite{ArtBek05HPL}},
pdf = {http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint234.pdf}
}
@incollection{ArtBek05HPL,
author = {Sergei N. Artemov and Lev D. Beklemishev},
title = {Provability Logic},
booktitle = {Handbook of Philosophical Logic, 2nd Edition},
publisher = {Springer},
year = {2005},
editor = {D[ov] M. Gabbay and F. Guenthner},
volume = {13},
pages = {189--360},
pdf = {http://www.cs.gc.cuny.edu/~sartemov/publications/ArtBeklRoot.pdf},
doi = {10.1007/1-4020-3521-7_3}
}
@unpublished{ArtBon06Unp,
author = {Sergei [N.] Artemov and Eduardo Bonelli},
title = {The Intensional Lambda Calculus},
note = {Extended version of~\cite{ArtBon07LFCS}},
year = {2006},
month = dec,
pdf = {http://www.lifia.info.unlp.edu.ar/~eduardo/lamIFull.pdf},
abstract = {We introduce a natural deduction formulation for the Logic of Proofs,
a refinement of modal logic~$\mathbf{S4}$ in which the assertion~$[]A$
is replaced by~$[[s]]A$ whose intended reading is ``$s$~\emph{is a proof of}~$A$''.
A term calculus for this formulation yields a typed lambda calculus~$\lambda^{\mathbf{I}}$
that internalises \emph{intensional} information on \emph{how} a term is computed.
In the same way that the Logic of Proofs internalises its own \emph{derivations},
$\lambda^{\mathbf{I}}$~internalises its own \emph{computations}.
Confluence and strong normalisation of~$\lambda^{\mathbf{I}}$ is proved.
This system serves as the basis for the study of type theories
that internalise intensional aspects of computation.}
}
@incollection{ArtBon07LFCS,
author = {Sergei [N.] Artemov and Eduardo Bonelli},
title = {The Intensional Lambda Calculus},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2007,
{N}ew {Y}ork, {NY}, {USA}, {J}une~4--7, 2007, Proceedings},
year = {2007},
editor = {Sergei N. Artemov and Anil Nerode},
volume = {4514},
series = {Lecture Notes in Computer Science},
pages = {12--25},
publisher = {Springer},
conference = {http://lfcs.info/lfcs07/},
doi = {10.1007/978-3-540-72734-7_2},
pdf = {http://www.lifia.info.unlp.edu.ar/~eduardo/publications/lfcs07.pdf},
abstract = {We introduce a natural deduction formulation for the Logic of Proofs,
a refinement of modal logic~$\mathbf{S4}$ in which the assertion~$[]A$
is replaced by~$[[s]]A$ whose intended reading is ``$s$~\emph{is a proof of}~$A$''.
A term calculus for this formulation yields a typed lambda calculus~$\lambda^{\mathbf{I}}$
that internalises \emph{intensional} information on \emph{how} a term is computed.
In the same way that the Logic of Proofs internalises its own \emph{derivations},
$\lambda^{\mathbf{I}}$~internalises its own \emph{computations}.
Confluence and strong normalisation of~$\lambda^{\mathbf{I}}$ is proved.
This system serves as the basis for the study of type theories
that internalise intensional aspects of computation.}
}
@techreport{ArtChu94TR,
author = {Sergei [N.] Art{\"{e}}mov and Art{\"{e}}m Chuprina},
title = {Logic of proofs with complexity operators},
institution = {Institute for Logic, Language and Computation, University of Amsterdam},
year = {1994},
number = {ML--1994--07},
note = {Later version published as~\cite{ArtChu96LNPAM}},
ps = {http://www.illc.uva.nl/Publications/ResearchReports/ML-1994-07.text.ps.gz}
}
@incollection{ArtChu96LNPAM,
author = {Sergei [N.] Art{\"{e}}mov and Art{\"{e}}m Chuprina},
title = {Logic of proofs with complexity operators},
booktitle = {Logic and Algebra},
publisher = {Marcel Dekker},
year = {1996},
address = {New York},
editor = {Aldo Ursini and Paolo Aglian{\`{o}}},
volume = {180},
series = {Lecture Notes in Pure and Applied Mathematics},
pages = {1--24},
distrweb = {http://www.crcpress.com/product/isbn/9780824796068},
review = {http://www.ams.org/mathscinet/pdf/1404932.pdf},
abstract = {The logic of proofs is the modal provability logic enriched by new operators (labeled modalities) for individual proofs.
In the current paper we add to the logic of proofs also new labeled modalities which stand for the complexity of proofs.
The Kripke style completeness, decidability, and arithmetical completeness theorems are obtained.
The complexity logics introduced here correspond to two major classes of complexity measures: decidable and recursively enumerable ones;
the completeness theorems relate either of these logics to the entire class of the relevant complexity measures.}
}
@incollection{ArtIem04TR,
author = {Sergei [N.] Artemov and Rosalie Iemhoff},
title = {From de {J}ongh's theorem to intuitionistic logic of proofs},
booktitle = {Vriendenboek ofwel {L}iber {A}micorum ter gelegenheid van het afscheid van {D}ick de {J}ongh},
publisher = {Institute for Logic, Language and Computation, University of Amsterdam},
year = {2004},
month = nov # {~22,},
pdf = {http://www.illc.uva.nl/D65/artemov.pdf},
http = {http://www.illc.uva.nl/D65/},
abstract = {The famous de Jongh's theorem of~1970 stated that the intuitionistic logic captured all the logical formulas
which have all arithmetical instances derivable in the Heyting Arithmetic~$\mathsf{HA}$.
In this note we extend de Jongh's arithmetical completeness property from~$\mathsf{IPC}$ to the basic intuitionistic logic of proofs,
which allows proof assertion statements of the sort $x$~\emph{is a proof of}~$F$.
The logic of proofs seems to provide an appropriate language of describing admissible rules in~HA.}
}
@techreport{ArtIem05TR,
author = {Sergei [N.] Artemov and Rosalie Iemhoff},
title = {The Basic Intuitionistic Logic of Proofs},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2005},
number = {TR--2005002},
month = feb,
note = {Later version published as~\cite{ArtIem07JSL}},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005002.pdf},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2005002.ps},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=153},
abstract = {The language of the basic logic of proofs extends the usual propositional language
by forming sentences of the sort $x$~\emph{is a proof of}~$F$ for any sentence~$F$.
In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic~$\mathsf{HA}$ was found.}
}
@article{ArtIem07JSL,
author = {Sergei [N.] Artemov and Rosalie Iemhoff},
title = {The Basic Intuitionistic Logic of Proofs},
journal = {Journal of Symbolic Logic},
year = {2007},
volume = {72},
number = {2},
pages = {439--451},
month = jun,
doi = {10.2178/jsl/1185803617},
ps = {http://www.phil.uu.nl/~iemhoff/logicproofs.ps},
review = {http://www.ams.org/mathscinet/pdf/2320284.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:05170333&type=pdf&format=complete},
abstract = {The language of the basic logic of proofs extends the usual propositional language
by forming sentences of the sort $x$~\emph{is a proof of}~$F$ for any sentence~$F$.
In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic~$\mathsf{HA}$ was found.}
}
@techreport{ArtKazSha99,
author = {S[ergei N.] Artemov and E. [L.] Kazakov and D. Shapiro},
title = {Logic of knowledge with justifications},
institution = {{C}ornell {U}niversity},
year = {1999},
number = {{CFIS} 99--12},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/S5LP.ps}
}
@inproceedings{ArtNKru06LC,
author = {Sergei [N.] Artemov and Nikolai [V.] Krupski},
title = {On Reflexive Combinatory Logic},
booktitle = {2005~Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'05,
{A}thens, {G}reece, {J}uly~28--{A}ugust~3, 2005},
year = {2006},
volume = {12(2)},
series = {Bulletin of Symbolic Logic},
pages = {351--352},
month = jun,
publisher = {Association for Symbolic Logic},
note = {Abstract presented by title},
ps = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps},
doi = {10.2178/bsl/1146620064},
abstract = {The Reflective Combinatory Logic~$\mathsf{RCL}$~\cite{Art04RMS} is an extension of the Typed Combinatory Logic~$\mathsf{CL}_{\rightarrow}$
which admits typing judgments of the form ``$t$~is a term of type~$F$'' inside types via an additional type constructor~$t:F$.
Unlike the case of the Intuitionistic Type Theory~[Mar98] where a similar type constructor is also available,
the type~$t:F$ in~$\mathsf{RCL}$ is inhabited by nontrivial terms that store a complete information about the typing judgment.
In the definition of~$\mathsf{RCL}$ the following two judgments have been introduced by simultaneous induction:
``$F$~is a well-formed formula (or type)'' and ``$F$~is derivable from $F_1,\ldots,F_n$''.
The intended meaning of the latter is ``type~$F$ is inhabited provided all types~$F_i$ are''.
In this talk we give an equivalent cut-free sequent formulation for~$\mathsf{RCL}$ and
establish complexity bounds for the decision problems concerning these judgements.
\textbf{Theorem 1}. \emph{The well-formedness property for~$\mathsf{RCL}$ is decidable in polynomial time.
The derivability in~$\mathsf{RCL}$ is decidable and PSPACE-complete.}}
}
@techreport{ArtVKru94TR,
author = {Sergei [N.] Art{\"{e}}mov and Vladimir [N.] Krupski},
title = {Referential data structures},
institution = {Institute of Computer Science and Applied Mathematics, University of Bern},
year = {1994},
number = {iam--94--020},
note = {Later version published as~\cite{ArtVKru94LFCS}},
psgza = {http://www.iam.unibe.ch/publikationen/techreports/1994/iam-94-020/file/at_download},
http = {http://www.iam.unibe.ch/publikationen/techreports/1994/iam-94-020},
abstract = {We introduce \emph{reference structures}~-- a basic logical model of a computer memory organization
capable to store and utilize information about its addresses.
The corresponding labeled modal logics are axiomatized and supplied with the completeness and decidability theorems.
A labeled modal formula can be regarded as a description of a certain reference structure;
the satisfiability algorithm gives a method of building and optimizing reference structures satisfying a given formula.}
}
@incollection{ArtVKru94LFCS,
author = {Sergei [N.] Art{\"{e}}mov and Vladimir [N.] Krupski},
title = {Referential data structures and labeled modal logic},
booktitle = {Logical Foundations of Computer Science, Third International Symposium, {LFCS}'94,
{St.~P}etersburg, {R}ussia, {J}uly 11--14, 1994, Proceedings},
year = {1994},
editor = {A[nil] Nerode and Yu. V. Matiyasevich},
volume = {813},
series = {Lecture Notes in Computer Science},
pages = {23--33},
publisher = {Springer},
doi = {10.1007/3-540-58140-5_4},
abstract = {We introduce \emph{reference structures}~-- a basic logical model of a computer memory organization
capable to store and utilize information about its addresses.
The corresponding labeled modal logics are axiomatized and supplied with the completeness and decidability theorems.
A labeled modal formula can be regarded as a description of a certain reference structure;
the satisfiability algorithm gives a method of building and optimizing reference structures satisfying a given formula.}
}
@techreport{ArtVKru95TR,
author = {Sergei [N.] Art{\"{e}}mov and Vladimir [N.] Krupski},
title = {Data storage interpretation of labeled modal logic},
institution = {Institute of Computer Science and Applied Mathematics, University of Bern},
year = {1995},
number = {iam--95--002},
note = {Later version published as~\cite{ArtVKru96APAL}},
psgza = {http://www.iam.unibe.ch/publikationen/techreports/1995/iam-95-002/file/at_download},
http = {http://www.iam.unibe.ch/publikationen/techreports/1995/iam-95-002},
abstract = {We introduce \emph{reference structures}~-- a basic mathematical model of a data organization
capable to store and utilize information about its addresses.
A propositional labeled modal language is used as a specification and programming language for reference structures;
the satisfiability algorithm for modal language gives a method of building and optimizing reference structures satisfying a given formula.
Corresponding labeled modal logics are presented, supplied with cut free axiomatizations, completeness and decidability theorems are proved.
Initialization of typed variables in some programming languages is presented as an example of a reference structure building.}
}
@article{ArtVKru96APAL,
author = {Sergei [N.] Art{\"{e}}mov and Vladimir [N.] Krupski},
title = {Data storage interpretation of labeled modal logic},
journal = {Annals of Pure and Applied Logic},
year = {1996},
volume = {78},
number = {1--3},
pages = {57--71},
month = apr,
doi = {10.1016/0168-0072(95)00062-3},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/APAL96.ps},
abstract = {We introduce \emph{reference structures}~-- a basic mathematical model of a data organization
capable to store and utilize information about its addresses.
A propositional labeled modal language is used as a specification and programming language for reference structures;
the satisfiability algorithm for modal language gives a method of building and optimizing reference structures satisfying a given formula.
Corresponding labeled modal logics are presented, supplied with cut free axiomatizations, completeness and decidability theorems are proved.
Initialization of typed variables in some programming languages is presented as an example of a reference structure building.}
}
@techreport{ArtKuz06TR,
author = {Sergei [N.] Artemov and Roman Kuznets},
title = {Logical Omniscience via Proof Complexity},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2006},
number = {TR--2006005},
month = may,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=182},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2006005.pdf},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2006005.ps},
note = {Later version published as~\cite{ArtKuz06CSL}},
abstract = {The Hintikka-style modal logic approach to knowledge has a well-known defect of logical omniscience,
i.e.,~an unrealistic feature that an agent knows all logical consequences of her assumptions.
In this paper we suggest the following Logical Omniscience Test~(LOT):
an epistemic system~$\mathsf{E}$ is not logically omniscient
if for any valid in~$\mathsf{E}$ knowledge assertion~$\mathcal{A}$ of type `$F$~\emph{is known}'
there is a proof of~$F$ in~$\mathsf{E}$,
the complexity of which is bounded by some polynomial in the length of~$\mathcal{A}$.
We show that the usual epistemic modal logics are logically omniscient (modulo some common complexity assumptions).
We also apply LOT to Justification Logic, which along with the usual knowledge operator~$K_i(F)$
(`\emph{agent~$i$ knows~$F$}') contain evidence assertions $t:F$ (`$t$~\emph{is a justification for}~$F$').
In Justification Logic, the evidence part is an appropriate extension of the Logic of Proofs~$\mathsf{LP}$,
which guarantees that the collection of evidence terms~$t$ is rich enough to match modal logic.
We show that justification logic systems are logically omniscient w.r.t.~the usual knowledge and
are not logically omniscient w.r.t.~the evidence-based knowledge.}
}
@incollection{ArtKuz06CSL,
author = {Sergei [N.] Artemov and Roman Kuznets},
title = {Logical Omniscience Via Proof Complexity},
booktitle = {{C}omputer {S}cience {L}ogic, 20th~International Workshop,
{CSL}~2006, 15th~Annual Conference of the {EACSL},
{S}zeged, {H}ungary, {S}eptember~25--29, 2006, Proceedings},
year = {2006},
editor = {Zolt{\'{a}}n {\'{E}}sik},
volume = {4207},
series = {Lecture Notes in Computer Science},
pages = {135--149},
publisher = {Springer},
conference = {http://www.inf.u-szeged.hu/~csl06/},
doi = {10.1007/11874683_9},
pdf = {http://sites.google.com/site/kuznets/CSL06.pdf},
abstract = {The Hintikka-style modal logic approach to knowledge contains a well-known defect of logical omniscience,
i.e.,~the unrealistic feature that an agent knows all logical consequences of her assumptions.
In this paper, we suggest the following Logical Omniscience Test~(LOT):
an epistemic system~E is not logically omniscient
if for any valid in~E knowledge assertion~A of type `F~is known,'
there is a proof of~F in~E,
the complexity of which is bounded by some polynomial in the length of~A.
We show that the usual epistemic modal logics are logically omniscient (modulo some common complexity assumptions).
We also apply LOT to evidence-based knowledge systems, which, along with the usual knowledge operator~$\mathrm{K_i}$(F)
(`agent~i knows~F'), contain evidence assertions~t:F (`t~is a justification for~F').
In evidence-based systems, the evidence part is an appropriate extension of the Logic of Proofs~LP,
which guarantees that the collection of evidence terms~t is rich enough to match modal logic.
We show that evidence-based knowledge systems are logically omniscient w.r.t.~the usual knowledge and
are not logically omniscient w.r.t.~evidence-based knowledge.}
}
@inproceedings{ArtKuz09TARK,
author = {Sergei [N.] Artemov and Roman Kuznets},
title = {Logical Omniscience as a Computational Complexity Problem},
booktitle = {Theoretical {A}spects of {R}ationality and {K}nowledge, Proceedings of the Twelfth Conference ({TARK~2009})},
year = {2009},
editor = {Aviad Heifetz},
pages = {14--23},
address = {Stanford University, California},
publisher = {ACM},
month = jul # { 6--8,},
doi = {10.1145/1562814.1562821},
conference = {http://ai.stanford.edu/~epacuit/tark09/},
abstract = {The logical omniscience feature assumes that an epistemic agent knows all logical consequences of her assumptions.
This paper offers a general theoretical framework that views logical omniscience as a computational complexity problem.
We suggest the following approach:
we assume that the knowledge of an agent is represented by an epistemic logical system~$E$;
we call such an agent \emph{not logically omniscient}
if for any valid knowledge assertion~$\mathcal{A}$ of type \emph{$F$~is known},
a proof of~$F$ in~$E$ can be found in polynomial time in the size of~$\mathcal{A}$.
We show that agents represented by major modal logics of knowledge and belief are logically omniscient,
whereas agents represented by justification logic systems are not logically omniscient with respect to
\emph{$t$~is a justification for~$F$}.}
}
@techreport{ArtNog04TR,
author = {Sergei [N.] Artemov and Elena Nogina},
title = {Logic of knowledge with justifications from the provability perspective},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2004},
number = {TR--2004011},
month = aug,
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004011.pdf},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2004011.ps},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=106},
note = {Later versions published as technical report~\cite{ArtNog05TR}, extended conference abstract~\cite{ArtNog05TARK}, and journal version~\cite{ArtNog05JLC}},
abstract = {An issue of a logic of knowledge with justifications has been discussed since the early~1990s.
Such a logic along with the usual knowledge operator~$[]F$ ``$F$~\emph{is known}''
should contain assertions~$t:F$ ``$t$~\emph{is an evidence of}~$F$''.
In this paper we build two systems of logic of knowledge with justifications:
$\mathsf{LPS4}$, which is an extension of the basic epistemic logic~$\mathsf{S4}$
by an appropriate calculus of evidences corresponding to the logic of proofs~$\mathsf{LP}$
together with the principle that justification implies knowledge,
and~$\mathsf{LPS4}^{--}$, which is $\mathsf{LPS4}$ augmented by the mixed implicit/explicit negative introspection principle.
We offer a provability semantics for~$\mathsf{LPS4}$ and~$\mathsf{LPS4}^{--}$
where the epistemic modality~$[]F$ is interpreted as ``$F$~\emph{is true and provable}''
and the evidence assertions~$t:F$ as ``$t$~\emph{is a proof of}~$F$''.
We find Kripke semantics and establish a number of fundamental properties of~$\mathsf{LPS4}$ and~$\mathsf{LPS4}^{--}$.
On the way to those systems we find the minimal joint logic of proofs and formal provability,~$\mathsf{LPGL}$,
complete with respect to the standard provability semantics.}
}
@techreport{ArtNog05TR,
author = {Sergei [N.] Artemov and Elena Nogina},
title = {Basic systems of epistemic logic with justification},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2005},
number = {TR--2005004},
month = feb,
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005004.pdf},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2005004.ps},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=151},
note = {Later versions published as extended conference abstract~\cite{ArtNog05TARK} and journal version~\cite{ArtNog05JLC}},
abstract = {An issue of an epistemic logic with justification has been discussed since the early~1990s.
Such a logic, along with the usual knowledge operator~$[]F$ ($F$~\emph{is known}),
should contain assertions~$t:F$ ($t$~\emph{is a justification for}~$F$),
which gives a more nuanced and realistic model of knowledge.
In this paper, we build two systems of epistemic logic with justification:
the minimal one--—$\mathsf{S4LP}$--—which is an extension of the basic epistemic logic~$\mathsf{S4}$
by an appropriate calculus of justification corresponding to the logic of proofs~$\mathsf{LP}$,
and~$\mathsf{S4LPN}$--—which is~$\mathsf{S4LP}$ augmented by the explicit negative introspection principle
$\neg(t:F) \to []\neg(t:F)$.
Epistemic semantics for both systems are suggested.
Completeness and specific properties of~$\mathsf{S4LP}$ and~$\mathsf{S4LPN}$,
reflecting the explicit character of those systems, are established.}
}
@inproceedings{ArtNog05TARK,
author = {Sergei [N.] Artemov and Elena Nogina},
title = {On Epistemic Logic with Justification},
booktitle = {Theoretical {A}spects of {R}ationality and {K}nowledge, Proceedings of the Tenth Conference ({TARK~2005})},
year = {2005},
editor = {Ron van der Meyden},
pages = {279--294},
address = {Singapore},
publisher = {National University of Singapore},
month = jun # { 10--12,},
note = {Journal version published as~\cite{ArtNog05JLC}},
conference = {http://www.tark.org/tark05.htm},
pdf = {http://www.tark.org/proceedings/tark_jul10_05/p279-artemov.pdf},
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 \emph{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$~\emph{is known}),
contains assertions~$t:F$ ($t$~\emph{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.}
}
@article{ArtNog05JLC,
author = {Sergei [N.] Artemov and Elena Nogina},
title = {Introducing Justification into Epistemic Logic},
journal = {Journal of Logic and Computation},
year = {2005},
volume = {15},
number = {6},
pages = {1059--1073},
month = dec,
doi = {10.1093/logcom/exi053},
review = {http://www.ams.org/mathscinet/pdf/2186735.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:05008192&type=pdf&format=complete},
keywords = {epistemic lgoic, logic of proofs, justification, knowledge},
abstract = {Plato's tripartite definition of knowledge as \emph{justified true belief}~(JTB) is generally regarded
as a set of necessary conditions for the possession of knowledge.
The \emph{true belief} components the JTB~definition are represented in formal epistemology
by modal logic and its possible worlds semantics.
At the same time, the \emph{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$~\emph{is known}),
contains assertions~$t:F$ ($t$~\emph{is a justification for}~$F$).
We study two basic systems, $\mathsf{S4LP}$ and~$\mathsf{S4LPN}$, of epistemic logic with justification and
show completeness with respect to natural epistemic semantics,
which augments Kripke models with a natural Fitting-style treatment of justification assertions~$t:F$.
Some new specific properties of epistemic logic with justification are established.}
}
@incollection{ArtNog08CSR,
author = {Sergei [N.] Artemov and Elena Nogina},
title = {Topological Semantics of Justification Logic},
booktitle = {Computer Science~--- Theory and Applications, Third International {C}omputer {S}cience Symposium in {R}ussia, {CSR~2008},
{M}oscow, {R}ussia, {J}une 7--12, 2008, Proceedings},
year = {2008},
editor = {Edward A. Hirsch and Alexander A. Razborov and Alexei Semenov and Anatol Slissenko},
volume = {5010},
series = {Lecture Notes in Computer Science},
pages = {30--39},
publisher = {Springer},
note = {Journal version published as~\cite{ArtNog08LLP}},
doi = {10.1007/978-3-540-79709-8_7},
conference = {http://csr2008.ru/},
keywords = {Justification Logic, Logic of Proofs, modal logic, topological semantics, Tarski},
abstract = {The Justification Logic is a family of logical systems obtained from epistemic logics by adding new type of formulas~$t:F$
which reads as $t$~\emph{is a justification for}~$F$.
The major epistemic modal logic~$\mathsf{S4}$ has a well-known Tarski topological interpretation
which interprets~$[]F$ as the interior of~$F$
(a topological equivalent of the `\emph{knowable part of}~$F$').
In this paper we extend the Tarski topological interpretation from epistemic modal logics
to justification logics which have both:
knowledge assertions~$[]F$ and justification assertions~$t:F$.
This topological semantics interprets modality as the interior, terms~$t$ represent tests,
and a justification assertion~$t:F$ represents a \emph{part of~$F$ which is accessible for test}~$t$.
We establish a number of soundness and completeness results with respect to Kripke topology and
the real line topology for $\mathsf{S4}$-based systems of Justification Logic.}
}
@article{ArtNog08LLP,
author = {Sergei [N.] Artemov and Elena Nogina},
title = {The Topology of Justification},
journal = {Logic and Logical Philosophy},
year = {2008},
volume = {17},
number = {1--2},
pages = {59--71},
month = mar # {/} # jun,
llp = {http://www.logika.umk.pl/llp/pi.html#n1712},
abstract = {Justification Logic is a family of epistemic logical systems obtained from modal logics of knowledge by adding a new type of formula~$t:F$~,
which is read $t$~\emph{is a justification for}~$F$.
The principal epistemic modal logic~$\mathsf{S4}$ includes Tarski's well-known topological interpretation,
according to which the modality~$[]X$ is read \emph{the Interior of~$X$ in a topological space}
(the topological equivalent of the `\emph{knowable part of}~$X$').
In this paper, we extend Tarski's topological interpretation from~$\mathsf{S4}$ to Justification Logic systems
with both modality and justification assertions.
The topological semantics interprets~$t:X$ as a reachable subset of~$X$
(the topological equivalent of `\emph{test~$t$ confirms~$X$}').
We establish a number of soundness and completeness results with respect to Kripke topology and
the real topology for $\mathsf{S4}$-based systems of Justification Logic.},
keywords = {modal logic, Justification Logic, topological semantics, Tarski}
}
@techreport{ArtStr92TR,
author = {Sergei [N.] Art{\"{e}}mov and Tyko Stra{\ss}en},
title = {The Basic Logic of Proofs},
institution = {Institute of Computer Science and Applied Mathematics, University of Bern},
year = {1992},
number = {iam--92--018},
http = {http://www.iam.unibe.ch/publikationen/techreports/1992/iam-92-018},
psgza = {http://www.iam.unibe.ch/publikationen/techreports/1992/iam-92-018/file/at_download},
note = {Later version published as~\cite{ArtStr93CSL}},
abstract = {Propositional Provability Logic was axiomatized in~[Sol76].
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{ArtStr93TR,
author = {Sergei [N.] Art{\"{e}}mov and Tyko Stra{\ss}en},
title = {Functionality in the Basic Logic of Proofs},
institution = {Institute of Computer Science and Applied Mathematics, University of Bern},
year = {1993},
number = {iam--93--004},
http = {http://www.iam.unibe.ch/publikationen/techreports/1993/iam-93-004},
psgza = {http://www.iam.unibe.ch/publikationen/techreports/1993/iam-93-004/file/at_download},
abstract = {This report describes the elimination of the injectivity restriction
for functional arithmetical interpretations as used in the systems~$\mathcal{PF}$ and~$\mathcal{PFM}$
in the Basic Logic of Proofs.
An appropriate axiom system~$\mathcal{PU}$ 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.}
}
@incollection{ArtStr93CSL,
author = {Sergei [N.] Art{\"{e}}mov and Tyko Stra{\ss}en},
title = {The Basic Logic of Proofs},
booktitle = {{C}omputer {S}cience {L}ogic, 6th Workshop, {CSL}'92,
{S}an {M}iniato, {I}taly, {S}eptember 28--{O}ctober 2, 1992, Selected Papers},
year = {1993},
editor = {E. B{\"{o}}rger and G. J{\"{a}}ger and Kleine B{\"{u}}ning, H. and S. Martini and M. M. Richter},
volume = {702},
series = {Lecture Notes in Computer Science},
pages = {14--28},
publisher = {Springer},
doi = {10.1007/3-540-56992-8_3},
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:00515725&type=pdf&format=complete},
abstract = {Propositional Provability Logic was axiomatized in~[Sol76].
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.}
}
@incollection{ArtStr93KGC,
author = {Sergei [N.] Art{\"{e}}mov and Tyko Stra{\ss}en},
title = {The Logic of the {G\"{o}}del Proof Predicate},
booktitle = {Computational Logic and Proof Theory, Third {K}urt {G\"{o}}del {C}olloquium, {KGC}'93,
{B}rno, {C}zech {R}epublic, {A}ugust 24--27, 1993, Proceedings},
year = {1993},
editor = {Georg Gottlob and Alexander Leitsch and Daniele Mundici},
volume = {713},
series = {Lecture Notes in Computer Science},
pages = {71--82},
publisher = {Springer},
doi = {10.1007/BFb0022556},
abstract = {We discuss the logics of the operators ``$p$~is a proof of~$A$'' and ``$p$~is a proof containing~$A$''
for the standard G{\"{o}}del proof predicate in Peano Arithmetic.
Decidabillty and arithmetical completeness of these logics are proved.
We use the same semantics as for the Provability Logic where the operator ``$A$~is provable'' is studied.}
}
@article{ArtTYav01MMJ,
author = {Sergei [N.] Artemov and Tatiana {Yavorskaya (Sidon)}},
title = {On First Order Logic of Proofs},
journal = {Moscow Mathematical Journal},
year = {2001},
volume = {1},
number = {4},
pages = {475--490},
month = oct # {-} # dec,
ams = {http://www.ams.org/distribution/mmj/vol1-4-2001/abst1-4-2001.html#artsidon_abstract},
pdf = {http://www.cs.gc.cuny.edu/~sartemov/publications/artsidon.pdf},
review = {http://www.ams.org/mathscinet/pdf/1901071.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:01751350&type=pdf&format=complete},
keywords = {logic of proofs, provability, recursive axiomatizability},
abstract = {The Logic of Proofs~$\mathsf{LP}$ solved long standing G{\"{o}}del's problem
concerning his provability calculus (cf.~\cite{Art01BSL}]).
It also opened new lines of research in proof theory, modal logic,
typed programming languages, knowledge representation, etc.
The propositional logic of proofs is decidable and admits a complete axiomatization.
In this paper we show that the first order logic of proofs is not recursively axiomatizable.}
}
@techreport{ArtTYav11TR,
author = {Sergei N. Artemov and Tatiana {Yavorskaya (Sidon)}},
title = {First-Order Logic of Proofs},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2011},
number = {TR--2011005},
month = may,
http = {http://tr.cs.gc.cuny.edu/tr/techreport.php?id=418},
pdf = {http://tr.cs.gc.cuny.edu/tr/files/TR-2011005.pdf},
abstract = {The propositional logic of proofs~$\mathsf{LP}$ revealed an explicit provability reading of modal logic~$\mathsf{S4}$
which provided an indented provability semantics for the propositional intuitionistic logic~$\mathsf{IPC}$ and led to a new area, Justification Logic.
In this paper, we find the \emph{first-order logic of proofs}~$\mathsf{FOLP}$ capable of realizing first-order modal logic~$\mathsf{S4}$ and,
therefore, the first-order intuitionistic logic~$\mathsf{HPC}$.
$\mathsf{FOLP}$ enjoys a natural provability interpretation;
this provides a semantics of explicit proofs for first-order~$\mathsf{S4}$ and~$\mathsf{HPC}$ compliant with Brouwer-Heyting-Kolmogorov requirements.
$\mathsf{FOLP}$~opens the door to a general theory of first-order justification.}
}
@incollection{BavBon10ICTAC,
author = {Francisco Bavera and Eduardo Bonelli},
title = {Justification Logic and History Based Computation},
booktitle = {Theoretical Aspects of Computing -- {ICTAC~2010}, 7th~International Colloquium,
{N}atal, {R}io {G}rande do {N}orte, {B}razil, {S}eptember 1-3, 2010, Proceedings},
publisher = {Springer},
year = {2010},
editor = {Ana Cavalcanti and David Deharbe and Marie-Claude Gaudel and Jim Woodcock},
volume = {6255},
series = {Lecture Notes in Computer Science},
pages = {337--351},
doi = {10.1007/978-3-642-14808-8_23},
conference = {http://www.iist.unu.edu/ICTAC/ictac2010/},
abstract = {Justification Logic~(JL) is a refinement of modal logic
that has recently been proposed for explaining well-known paradoxes
arising in the formalization of Epistemic Logic.
Assertions of knowledge and belief are accompanied by justifications:
the formula~$[[t]]A$ states that $t$~is ``reason'' for knowing/believing~$A$.
We study the computational interpretation of~JL via the Curry-de Bruijn-Howard isomorphism
in which the modality~$[[t]]A$ is interpreted as:
$t$~is a type derivation justifying the validity of~$A$.
The resulting lambda calculus is such that its terms are aware of the reduction sequence
that gave rise to them.
This serves as a basis for understanding systems, many of which belong to the security domain,
in which computation is history-aware.}
}
@techreport{BekVis05PR,
author = {Lev D. Beklemishev and Albert Visser},
title = {Problems in the Logic of Provability},
institution = {{L}ogic {G}roup {P}reprint {S}eries, {D}epartment of {P}hilosophy, {U}trecht {U}niversity},
year = {2005},
type = {Preprint},
number = {235},
month = may,
note = {Later version published as \cite{BekVis06IMS}},
pdf = {http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint235.pdf},
abstract = {In the first part of the paper we discuss some conceptual problems related to the notion of proof.
In the second part we survey five major open problems in Provability Logic
as well as possible directions for future research in this area.}
}
@incollection{BekVis06IMS,
author = {Lev [D.] Beklemishev and Albert Visser},
title = {Problems in the Logic of Provability},
booktitle = {Mathematical Problems from Applied Logic {I}, Logics for the {XXI}st Century},
publisher = {Springer},
year = {2006},
editor = {Dov M. Gabbay and Sergei S. Goncharov and Michael Zakharyaschev},
volume = {4},
series = {International Mathematical Series},
pages = {77--136},
doi = {10.1007/0-387-31072-X_2}
}
@incollection{vanBen06PS,
author = {van Benthem, Johan},
title = {Epistemic Logic and Epistemology: The State of their Affairs},
booktitle = {8 Bridges between Formal and Mainstream Epistemology},
publisher = {Springer},
year = {2006},
editor = {Vincent F. Hendricks},
volume = {128(1)},
series = {Philosophical Studies},
pages = {49--76},
month = mar,
doi = {10.1007/s11098-005-4052-0},
pdf = {http://www.illc.uva.nl/Publications/ResearchReports/PP-2005-20.text.pdf}
}
@incollection{vanBenMar08HPI,
author = {van Benthem, Johan and Maricarmen Martinez},
title = {The Stories of Logic and Information},
booktitle = {Philosophy of Information},
publisher = {Elsevier},
year = {2008},
editor = {Pieter Adriaans and van Benthem, Johan},
volume = {8},
series = {Handbook of the Philosophy of Science},
pages = {217--280},
doi = {10.1016/B978-0-444-51726-5.50012-1},
pdf = {http://www.illc.uva.nl/Publications/ResearchReports/PP-2008-04.text.pdf}
}
@incollection{BonFel09LFCS,
author = {Eduardo Bonelli and Federico Feller},
title = {The {L}ogic of {P}roofs as a Foundation for Certifying Mobile Computation},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2009,
{D}eerfield {B}each, {FL}, {USA}, {J}anuary 3--6, 2009, Proceedings},
publisher = {Springer},
year = {2009},
editor = {Sergei [N.] Artemov and Anil Nerode},
volume = {5407},
series = {Lecture Notes in Computer Science},
pages = {76--91},
note = {Errata available at \url{http://www.lifia.info.unlp.edu.ar/~eduardo/publications/errataLFCS09.txt}},
abstract = {We explore an intuitionistic fragment of Art{\"{e}}mov's \emph{Logic of Proofs}
as a type system for a programming language for \emph{mobile units}.
Such units consist of both a code and certificate component.
Dubbed the \emph{Certifying Mobile Calculus},
our language caters for both code and certificate development in a unified theory.
In the same way that mobile code is constructed
out of code components and extant type systems track local resource usage to ensure the mobile nature of these components,
our system \emph{additionally} ensures correct \emph{certificate construction} out of certificate components.
We present proofs of type safety and strong normalistion for a run-time system based on an abstract machine.},
conference = {http://lfcs.info/lfcs09/},
doi = {10.1007/978-3-540-92687-0_6}
}
@unpublished{BonFel09Unp,
author = {Eduardo Bonelli and Federico Feller},
title = {The {L}ogic of {P}roofs as a Foundation for Certifying Mobile Computation},
note = {Extended version of~\cite{BonFel09LFCS}},
year = {2009},
abstract = {We explore an intuitionistic fragment of Art{\"{e}}mov's \emph{Logic of Proofs}
as a type system for a programming language for \emph{mobile units}.
Such units consist of both a code and certificate component.
Dubbed the \emph{Certifying Mobile Calculus},
our language caters for both code and certificate development in a unified theory.
In the same way that mobile code is constructed
out of code components and extant type systems track local resource usage to ensure the mobile nature of these components,
our system \emph{additionally} ensures correct \emph{certificate construction} out of certificate components.
We present proofs of type safety and strong normalistion for a run-time system based on an abstract machine.},
pdf = {http://www.lifia.info.unlp.edu.ar/~eduardo/publications/lpCertFull.pdf}
}
@mastersthesis{Bre99MT,
author = {Vladimir N. Brezhnev},
title = {Explicit Counterparts of Modal Logic},
school = {Lomonosov Moscow State University, Faculty of Mechanics and Mathematics},
year = {1999},
note = {In Russian}
}
@techreport{Bre00TR,
author = {Vladimir N. Brezhnev},
title = {On explicit counterparts of modal logics},
institution = {Cornell University},
year = {2000},
number = {CFIS 2000--05},
abstract = {The epistemic meaning of modality suggests that a modal formula~$[]A \to []B$
implicitely specifies a function~$f(x)$ such that
if $x$~is a justification of~$A$ then $f(x)$~is a justification for~$B$.
S.~Artemov in~\cite{Art95TR}, \cite{Art01BSL} made this consideration formal
by introducing a system of \emph{proof polynomials} necessary and sufficient
for realizing modalities in every $S4$-derivation.
Proof polynomials subsume typed $\lambda$-calculus by allowing types depending on terms.
The Curry-Howard semantics of $\lambda$-terms as operations on proofs has also been extended to proof polynimials,
which answered a long standing question about the intended provability meaning of~$S4$.
Artemov’s Logic of Proofs~$\mathcal{LP}$
that desicribes all identities on proof polynomials may be regarded as an explicit counterpart of~$S4$.\\
In this paper we find explicit counterparts of the modal logics~$K$, $K4$, $T$, $D$ and~$D4$.
Realizing terms for all these logics are proper subclasses of proof polynomials.
The corresponding explicit modal logics are subsystems of~$\mathcal{LP}$.
The realization methods are based on the Artemov’s realization algorithm.}
}
@inproceedings{Bre01ESSLLI,
author = {Vladimir [N.] Brezhnev},
title = {On the Logic of Proofs},
booktitle = {Proceedings of the sixth {ESSLLI} Student Session,
13th {E}uropean {S}ummer {S}chool in {L}ogic, {L}anguage and {I}nformation ({ESSLLI'}01)},
year = {2001},
month = aug,
address = {{H}elsinki},
editor = {Kristina Striegnitz},
organization = {{FoLLI}},
pages = {35--46},
pdf = {http://folli.loria.fr/cds/2001/courses/readers/studentsession.pdf#page=42},
conference = {http://cs.union.edu/~striegnk/esslli01/},
abstract = {The Logic of Proofs~($\mathbf{LP}$) was introduced by S.~N.~Artemov.
It is a system in the propositional language with additional sort of objects~--
proof terms, and an extra atomic propositions~$[t]F$ with intended reading ``$t$~is a proof of~$F$''.
$\mathbf{LP}$~is an explicit counterpart of modal logic~$\mathbf{S4}$,
since $\mathbf{S4}$~is the exact term-forgetting projection of~$\mathbf{LP}$.
In the present paper we build sequent system corresponding to fragment of~$\mathbf{LP}$ sufficient to realize~$\mathbf{S4}$.
Using its format we build explicit counterparts of modal logics~$\mathbf{K}$, $\mathbf{K4}$, $\mathbf{D}$, $\mathbf{D4}$ and~$\mathbf{T}$.
Also we define versions of this systems for which the intended interpretation of terms is proof tactics,
computable procedures able to find proofs of some formulas, having formula as input.}
}
@techreport{BreKuz05TR,
author = {Vladimir [N.] Brezhnev and Roman Kuznets},
title = {Making Knowledge Explicit: How Hard It Is},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2005},
number = {TR--2005003},
month = feb,
note = {Later version published as~\cite{BreKuz06TCS}},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=152},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005003.pdf},
abstract = {Artemov's logic of proofs~$\mathsf{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~$\mathsf{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~$\mathsf{LP}$ is its ability to realize modalities in any $\mathsf{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 $\mathsf{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~$\mathsf{S4}$ is inherently self-referential.}
}
@article{BreKuz06TCS,
author = {Vladimir [N.] Brezhnev and Roman Kuznets},
title = {Making Knowledge Explicit: How Hard It Is},
journal = {Theoretical Computer Science},
year = {2006},
volume = {357},
number = {1--3},
pages = {23--34},
month = jul,
doi = {10.1016/j.tcs.2006.03.010},
pdf = {http://sites.google.com/site/kuznets/BrezhnevKuznets06TCS.pdf},
review = {http://www.ams.org/mathscinet/pdf/2242755.pdf},
keywords = {logic of proofs, self-reference, modal logic},
abstract = {Artemov's logic of proofs~$\mathsf{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~$\mathsf{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~$\mathsf{LP}$ is its ability to realize modalities in any $\mathsf{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 $\mathsf{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~$\mathsf{S4}$ is inherently self-referential.}
}
@incollection{BrueGoeKuz10AiML,
author = {Kai Br{\"u}nnler and Remo Goetschi and Roman Kuznets},
title = {A Syntactic Realization Theorem for Justification Logics},
booktitle = {Advances in Modal Logic, Volume 8},
publisher = {College Publications},
year = {2010},
editor = {Lev [D.] Beklemishev and Valentin Goranko and Valentin Shehtman},
pages = {39--58},
conference = {http://aiml10.mi.ras.ru},
pubweb = {http://www.collegepublications.co.uk/aiml/?00005},
pdf = {http://www.aiml.net/volumes/volume8/Bruennler-Goetschi-Kuznets.pdf},
slides = {http://aiml10.mi.ras.ru/slides/goetschi.pdf},
keywords = {justification logic, modal logic, realization theorem, nested sequents, positive introspection},
abstract = {Justification logics are refinements of modal logics where modalities are replaced by justification terms.
They are connected to modal logics via so-called realization theorems.
We present a syntactic proof of a single realization theorem
that uniformly connects all the normal modal logics formed from the axioms~$\mathsf{d}$, $\mathsf{t}$, $\mathsf{b}$, $\mathsf{4}$, and~$\mathsf{5}$ with their justification counterparts.
The proof employs cut-free nested sequent systems together with Fitting's realization merging technique.
We further strengthen the realization theorem for $\mathsf{KB5}$~and~$\mathsf{S5}$ by showing that the positive introspection operator is superfluous.}
}
@incollection{Bry05M4M,
author = {Yegor Bryukhov},
title = {Automatic Proof Search in Logic of Justified Common Knowledge},
booktitle = {Proceedings of the 4th~Workshop ``Methods for Modalities'' ({M4M'}05),
{B}erlin, {G}ermany, {De}cember 1--2, 2005},
publisher = {Humboldt-{U}niversit{\"{a}}t zu {B}erlin, {I}nstitut f{\"{u}}r {I}nformatik},
year = {2005},
editor = {H. Schlingloff},
number = {194},
series = {Informatik-{B}erichte},
month = dec,
pages = {187--201},
conference = {http://m4m.loria.fr/M4M4/workshop.html},
pdf = {http://yegor.org/publications/m4m2005.pdf},
proceedings = {http://www2.informatik.hu-berlin.de/sam/preprint/schlingloff194.pdf},
http = {http://www.informatik.hu-berlin.de/institut/dokumente/preprint_html#2005},
abstract = {We consider the logic of justified common knowledge~$\mathsf{S4}_n^{\mathsf{J}}$ introduced in~\cite{Art04TR}.
This system captures the notion of \emph{justified common knowledge},
which is free of some of the deficiencies of the usual common knowledge operator,
and yet sufficient for analysis of epistemic problems where common knowledge has been traditionally applied.
In particular, $\mathsf{S4}_n^{\mathsf{J}}$~enjoys cut-elimination,
which opens a possibility for an automatic proof search in logic of common knowledge.
In this paper, we present an implementation that automatically builds cut-free proofs in~$\mathsf{S4}_n^{\mathsf{J}}$.
Our work is based on the existing matrix-based prover for intuitionistic logic~[SchLorKreNog01].}
}
@phdthesis{Bry06PhD,
author = {Yegor Bryukhov},
title = {Integration of Decision Procedures into High-Order Interactive Provers},
school = {CUNY Graduate Center},
year = {2006},
pdf = {http://yegor.org/publications/YegorBryukhovThesis2006.pdf},
abstract = {An efficient proof assistant uses a wide range of decision procedures,
including automatic verification of validity of arithmetical formulas with linear terms.
Since the final product of a proof assistant is a formalized and verified proof,
it prompts an additional task of building proofs of formulas,
which validity is established by such a decision procedure.
We present an implementation of several decision procedures for arithmetical formulas with linear terms
in the MetaPRL proof assistant in a way that provides formal proofs of formulas found valid by those procedures.
We also present an implementation of a theorem prover for the logic of justified common knowledge~$\mathsf{S4}_n^{\mathsf{J}}$
introduced in~\cite{Art04TR}.
This system captures the notion of \emph{justified common knowledge},
which is free of some of the deficiencies of the usual common knowledge operator,
and is yet sufficient for the analysis of epistemic problems where common knowledge has been traditionally applied.
In particular, $\mathsf{S4}_n^{\mathsf{J}}$~enjoys cut-elimination,
which introduces the possibility of automatic proof search in the logic of common knowledge.
Our implementation automatically builds cut-free sequent proofs in~$\mathsf{S4}_n^{\mathsf{J}}$.
This prover is based on the existing matrix-based prover for intuitionistic logic~[SchLorKreNog01].}
}
@incollection{BucKuzRenSacStu10LogKCA,
author = {Samuel Bucheli and Roman Kuznets and Bryan Renne and Joshua Sack and Thomas Studer},
title = {Justified Belief Change},
booktitle = {{LogKCA-10}, Proceedings of the Second {ILCLI} International Workshop on Logic and Philosophy of Knowledge, Communication and Action},
publisher = {University of the Basque Country Press},
year = {2010},
editor = {Xabier Arrazola and Mar{\'{\i}}a Ponte},
pages = {135--155},
keywords = {justification logic, dynamic epistemic logic, public announcements, belief revision},
pdf = {http://www.iam.unibe.ch/~tstuder/papers/bkrss-justifiedBeliefChange.pdf},
conference = {http://www.ilcli.ehu.es/p287-content/en/contenidos/informacion/ilcli_conferences/en_confe/conferences.html},
abstract = {Justification Logic is a framework for reasoning about evidence and justification.
Public Announcement Logic is a framework for reasoning about belief changes caused by public announcements.
This paper develops~$\mathsf{JPAL}$,
a dynamic justification logic of public announcements
that corresponds to the modal theory of public announcements due to Gerbrandy and Groeneveld.
$\mathsf{JPAL}$~allows us to reason about evidence brought about by and changed by Gerbrandy--Groeneveld-style public announcements.}
}
@incollection{BucKuzStu10M4M,
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
title = {Two Ways to Common Knowledge},
booktitle = {Proceedings of the 6th~Workshop on {M}ethods for {Modalities} ({M4M--6~2009}),
{C}openhagen, {D}enmark, 12--14 {N}ovember 2009},
publisher = {Elsevier},
year = {2010},
editor = {Thomas Bolander and Torben Bra{\"{u}}ner},
number = {262},
series = {Electronic Notes in Theoretical Computer Science},
pages = {83--98},
month = may,
keywords = {justification logics, common knowledge, proof theory},
doi = {10.1016/j.entcs.2010.04.007},
conference = {http://m4m.loria.fr/M4M6/},
pdf = {http://sites.google.com/site/kuznets/M4M09.pdf},
abstract = {It is not clear what a system for evidence-based common knowledge should look like
if common knowledge is treated as a greatest fixed point.
This paper is a preliminary step towards such a system.
We argue that the standard induction rule is not well suited to axiomatize evidence-based common knowledge.
As an alternative, we study two different deductive systems for the logic of common knowledge.
The first system makes use of an induction axiom whereas the second one is based on co-inductive proof theory.
We show the soundness and completeness for both systems.}
}
@techreport{BucKuzStu10TR,
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
title = {Explicit Evidence Systems with Common Knowledge},
institution = {arXiv.org},
year = {2010},
number = {1005.0484},
type = {E-print},
month = may,
note = {Later version published as~\cite{BucKuzStu11JANCL}},
eprint = {1005.0484},
pdf = {http://arxiv.org/pdf/1005.0484v1},
abstract = {Justification logics are epistemic logics that explicitly include justifications for the agents' knowledge.
We develop a multi-agent justification logic with evidence terms for individual agents as well as for common knowledge.
We define a Kripke-style semantics that is similar to Fitting's semantics for the Logic of Proofs~$\mathsf{LP}$.
We show the soundness, completeness, and finite model property of our multi-agent justification logic with respect to this Kripke-style semantics.
We demonstrate that our logic is a conservative extension of Yavorskaya's minimal bimodal explicit evidence logic, which is a two-agent version of~$\mathsf{LP}$.
We discuss the relationship of our logic to the multi-agent modal logic~$\mathsf{S4}$ with common knowledge.
Finally, we give a brief analysis of the coordinated attack problem in the newly developed language of our logic.}
}
@article{BucKuzStu11JANCL,
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
title = {Justifications for common knowledge},
journal = {Journal of Applied Non-Classical Logics},
year = {2011},
volume = {21},
number = {1},
pages = {35--60},
month = jan # {--} # mar,
doi = {10.3166/JANCL.21.35-60},
pdf = {http://www.iam.unibe.ch/~tstuder/papers/EESWCK.pdf},
keywords = {justification logic, epistemic modal logic, multi-agent systems, common knowledge},
abstract = {Justification logics are epistemic logics that explicitly include justifications for the agents' knowledge.
We develop a multi-agent justification logic with evidence terms for individual agents as well as for common knowledge.
We define a Kripke-style semantics that is similar to Fitting's semantics for the Logic of Proofs~$\mathsf{LP}$.
We show the soundness, completeness, and finite model property of our multi-agent justification logic with respect to this Kripke-style semantics.
We demonstrate that our logic is a conservative extension of Yavorskaya's minimal bimodal explicit evidence logic, which is a two-agent version of~$\mathsf{LP}$.
We discuss the relationship of our logic to the multi-agent modal logic~$\mathsf{S4}$ with common knowledge.
Finally, we give a brief analysis of the coordinated attack problem in the newly developed language of our logic.}
}
@incollection{BucKuzStu11WoLLIC,
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
title = {Partial Realization in Dynamic Justification Logic},
booktitle = {{L}ogic, {L}anguage, {I}nformation and {C}omputation, 18th~International {W}orkshop, {WoLLIC~2011},
{P}hiladelphia, {PA}, {USA}, {M}ay 18--20, 2011, Proceedings},
publisher = {Springer},
year = {2011},
editor = {Lev D. Beklemishev and Ruy de Queiroz},
volume = {6642},
series = {Lecture Notes in Artificial Intelligence},
pages = {35--51},
doi = {10.1007/978-3-642-20920-8_9},
conference = {http://wollic.org/wollic2011/},
pdf = {http://www.iam.unibe.ch/~tstuder/papers/wollic2011.pdf},
abstract = {Justification logic is an epistemic framework that provides a way to express explicit justifications for the agent's belief.
In this paper, we present~OPAL, a dynamic justification logic that includes term operators to reflect public announcements on the level of justifications.
We create dynamic epistemic semantics for~OPAL.
We also elaborate on the relationship of dynamic justification logics to Gerbrandy--Groeneveld's~PAL by providing a partial realization theorem.}
}
@incollection{BusKuz09LFCS,
author = {Samuel R. Buss and Roman Kuznets},
title = {The {NP}-Completeness of Reflected Fragments of Justification Logics},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2009,
{D}eerfield {B}each, {FL}, {USA}, {J}anuary 3--6, 2009, Proceedings},
publisher = {Springer},
year = {2009},
editor = {Sergei [N.] Artemov and Anil Nerode},
volume = {5407},
series = {Lecture Notes in Computer Science},
pages = {122--136},
conference = {http://lfcs.info/lfcs09/},
doi = {10.1007/978-3-540-92687-0_9},
pdf = {http://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/rlp_lower16_finalLFCS.pdf},
slides = {http://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/rlp_lower_LFCS09_talkslides.pdf},
abstract = {Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms.
Pure justification logics serve as counterparts of traditional modal epistemic logics,
and hybrid logics combine epistemic modalities with justification terms.
The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics.
Moreover, the so-called reflected fragments,
which still contain complete information about the respective justification logics,
are known to be in~NP for a wide range of justification logics,
pure and hybrid alike.
This paper shows that,
under reasonable additional restrictions,
these reflected fragments are NP-complete,
thereby proving a matching lower bound.}
}
@unpublished{BusKuz09Unp,
author = {Samuel R. Buss and Roman Kuznets},
title = {Lower Complexity Bounds in {J}ustification {L}ogic},
note = {Extended version of~\cite{BusKuz09LFCS}, submitted for publication},
year = {2009},
month = apr,
pdf = {http://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/APAL09_v12.pdf},
abstract = {Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms.
Pure justification logics serve as counterparts of traditional modal epistemic logics,
and hybrid logics combine epistemic modalities with justification terms.
The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics.
Moreover, the so-called reflected fragments,
which still contain complete information about the respective justification logics,
are known to be in~NP for a wide range of justification logics,
pure and hybrid alike.
This paper shows that,
under reasonable additional restrictions,
these reflected fragments are NP-complete,
thereby proving a matching lower bound.
The proof method is then extended to provide a uniform proof that the corresponding full pure justification logics are $\Pi^p_2$-hard,
reproving and generalizing an earlier result by Milnikel.}
}
@techreport{Das08PR,
author = {Evgenij Dashkov},
title = {Intuitionistic Logic of Proofs},
institution = {{L}ogic {G}roup {P}reprint {S}eries, {D}epartment of {P}hilosophy, {U}trecht {U}niversity},
year = {2008},
type = {Preprint},
number = {269},
month = nov,
pdf = {http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint269.pdf}
}
@article{Das09JLC,
author = {Evgenij Dashkov},
title = {Arithmetical Completeness of the Intuitionistic Logic of Proofs},
journal = {Journal of Logic and Computation},
year = {2009},
volume = {Advanced Access},
number = {},
pages = {},
month = aug,
note = {},
doi = {10.1093/logcom/exp041},
keywords = {logic of proofs, intuitionistic arithmetic, admissible rules},
abstract = {Classical logic of proofs~LP naturally extends propositional calculus
to the language enriched with formulas meaning \emph{$t$~is a proof of formula~$F$}.
Intuitionistic logic of proofs~iLP introduced by Artemov and Iemhoff was conjectured to be complete
with respect to intuitionistic arithmetic~HA.
The article presents a proof of this conjecture.}
}
@article{DeaKur10Synthese,
author = {W[alter] Dean and H[idenori] Kurokawa},
title = {From the {K}nowability {P}aradox to the existence of proofs},
journal = {Synthese},
year = {2010},
volume = {176},
number = {2},
pages = {177--225},
month = sep,
note = {Published online May~2009},
doi = {10.1007/s11229-009-9490-3},
keywords = {Knowability Paradox, Fitch, verificationism, intuitionistic logic, BHK interpretation, existence predicate, logic of proofs, potential proof, bivalence},
abstract = {The Knowability Paradox purports to show that the controversial but not patently absurd hypothesis
that all truths are knowable entails the implausible conclusion that all truths are known.
The notoriety of this argument owes to the negative light
it appears to cast on the view that there can be no verification-transcendent truths.
We argue that it is overly simplistic to formalize the views of contemporary verificationists
like Dummett, Prawitz or Martin-L{\"{o}}f using the sort of propositional modal operators
which are employed in the original derivation of the Paradox.
Instead we propose that the central tenet of verificationism is most accurately formulated as follows:
\emph{if $\varphi$~is true, then there exists a proof of~$\varphi$}.
Building on the work of Artemov~\cite{Art01BSL},
a system of explicit modal logic with proof quantifiers is introduced to reason about such statements.
When the original reasoning of the Paradox is developed in this setting,
we reach not a contradiction, but rather the conclusion that there must exist non-constructed proofs.
This outcome is evaluated relative to the controversy between Dummett and Prawitz about proof existence and bivalence.}
}
@inproceedings{DeaKur09FEW,
author = {Walter Dean and Hidenori Kurokawa},
title = {Knowledge, proof and the {K}nower},
booktitle = {Online Proceedings of Sixth Annual {F}ormal {E}pistemology {W}orkshop ({FEW~2009})},
year = {2009},
address = {Carnegie Mellon University, Pittsburg, PA, USA},
month = jun # { 18--21,},
note = {Later version published as~\cite{DeaKur09TARK}; comments by H.~Arl{\'{o}}-Costa and K.~Kishida available as~\cite{ArlKis09FEW}},
conference = {http://fitelson.org/few/few_09/},
pdf = {http://fitelson.org/few/few_09/dean_kurokowa.pdf},
slides = {http://fitelson.org/few/few_09/dean_kurokowa_slides.pdf},
abstract = {The Knower Paradox demonstrates that any theory~$T$ which
1)~extends Robinson arithmetic~$\mathsf{Q}$,
2)~includes a predicate~$K(x)$ intended to formalize
``the formula with godel number~$x$ is known by agent~$i$,'' and
3)~contains certain elementary epistemic principles involving~$K(x)$
is inconsistent.
The purpose of this paper is to show how this paradox may be redeveloped
within a system of quantified explicit modal logic in the tradition of Artemov~\cite{Art01BSL} and Fitting~\cite{Fit04TRb}, \cite{Fit05APAL}
which we argue allows for a more faithful formulation of some of the epistemic principles on which it is based.
Along the way, we isolate a principle -- the so-called Uniform Barcan Formula~[UBF] --
which we show is required to derive an explicit counterpart of the axiom~$\mathbf{U}$
(i.e.~$K(\lceil K(\lceil\varphi\rceil) \to \varphi\rceil)$)
which was used in the original formulation of the Paradox.
We argue that since there are independent epistemic reasons to be suspicious of~UBF,
the paradox may be resolved by abandoning this principle (and thereby~$\mathbf{U}$ as well).}
}
@inproceedings{DeaKur09TARK,
author = {Walter Dean and Hidenori Kurokawa},
title = {Knowledge, proof and the {K}nower},
booktitle = {Theoretical {A}spects of {R}ationality and {K}nowledge, Proceedings of the Twelfth Conference ({TARK~2009})},
year = {2009},
editor = {Aviad Heifetz},
pages = {81--90},
address = {Stanford University, California},
publisher = {ACM},
month = jul # { 6--8,},
doi = {10.1145/1562814.1562828},
conference = {http://ai.stanford.edu/~epacuit/tark09/},
abstract = {The Knower Paradox demonstrates that any theory~$T$ which
1)~extends Robinson arithmetic~$\mathsf{Q}$,
2)~includes a predicate~$K(x)$ intended to formalize
``the formula with godel number~$x$ is known by agent~$i$,'' and
3)~contains certain elementary epistemic principles involving~$K(x)$
is inconsistent.
The purpose of this paper is to show how this paradox may be redeveloped
within a system of quantified explicit modal logic in the tradition of Artemov~\cite{Art01BSL} and Fitting~\cite{Fit04TRb}, \cite{Fit05APAL}
which we argue allows for a more faithful formulation of some of the epistemic principles on which it is based.
Along the way, we isolate a principle -- the so-called Uniform Barcan Formula~[UBF] --
which we show is required to derive an explicit counterpart of the axiom~$\mathbf{U}$
(i.e.~$K(\lceil K(\lceil\varphi\rceil) \to \varphi\rceil)$)
which was used in the original formulation of the Paradox.
We argue that since there are independent epistemic reasons to be suspicious of~UBF,
the paradox may be resolved by abandoning this principle (and thereby~$\mathbf{U}$ as well).}
}
@article{Fin10JLC,
author = {Marcelo Finger},
title = {Analytic Methods for the Logic of Proofs},
journal = {Journal of Logic and Computation},
year = {2010},
volume = {20},
number = {1},
pages = {167--188},
month = feb,
doi = {10.1093/logcom/exn065},
note = {Published online November~2008},
pdf = {http://www.ime.usp.br/%7Emfinger/home/papers/Fin08.pdf},
keywords = {Logic of proofs, tableaux, KE tableaux},
abstract = {The logic of proofs~(LP) was proposed as G{\"{o}}del’s missed link between Intuitionistic and S4-proofs,
but so far the tableau-based methods proposed for~LP have not explored this closeness with~S4 and contain rules whose analycity is not immediately evident.
We study possible formulations of analytic tableau proof methods for~LP that preserve the subformula property.
Two sound and complete tableau decision methods of increasing degree of analycity are proposed, KELP and~\textsc{pre}KELP.
The latter is particularly inspired on S4-proofs. The crucial role of proof constants in the structure of LP-proofs methods is analysed.
In particular, a method for the abduction of proof constant specifications in strongly analytic \textsc{pre}KELP~proofs is presented;
abduction heuristics and the complexity of the method are discussed.}
}
@techreport{Fit03TRa,
author = {Melvin Fitting},
title = {A Semantic Proof of the Realizability of Modal Logic in the {L}ogic of {P}roofs},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2003},
number = {TR--2003010},
month = sep,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=85},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2003010.pdf}
}
@techreport{Fit03TRb,
author = {Melvin Fitting},
title = {A Semantics for the {L}ogic of {P}roofs},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2003},
number = {TR--2003012},
month = sep,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=86},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2003012.pdf}
}
@techreport{Fit04TRa,
author = {Melvin Fitting},
title = {Semantics and Tableaus for {LPS4}},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2004},
number = {TR--2004016},
month = oct,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=118},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004016.pdf},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2004016.ps},
abstract = {An axiomatic formulation of a logic called~$\mathbf{LPS4}$ appears in~\cite{ArtNog04TR}.
Here that logic is proved sound and complete with respect to the weak semantics of~\cite{Fit05APAL}.
Also a tableau system for~$\mathbf{LPS4}$ is introduced,
and also proved sound and complete with respect to the semantics,
thus establishing both cut elimination and equivalence with the axiomatic formulation.}
}
@techreport{Fit04TRb,
author = {Melvin Fitting},
title = {Quantified {LP}},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2004},
number = {TR--2004019},
month = dec,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=146},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004019.pdf},
abstract = {An extension,~$\mathbf{QLP}$, of the propositional logic of explicit proofs,~$\mathbf{LP}$,
is created, allowing quantification over proofs.
The resulting logic is given an axiomatization, a Kripke-style semantics, and soundness and completeness are shown.
It is shown that $\mathbf{S4}$~embeds into the logic,
when we translate the necessity operator using a quantifier:
there exists an explicit proof.
And it is shown that the propositional part of~$\mathbf{QLP}$ is exactly~$\mathbf{LP}$.
No connection with arithmetic provability is made.}
}
@article{Fit05APAL,
author = {Melvin Fitting},
title = {The logic of proofs, semantically},
journal = {Annals of Pure and Applied Logic},
year = {2005},
volume = {132},
number = {1},
pages = {1--25},
month = feb,
doi = {10.1016/j.apal.2004.04.009},
review = {http://www.ams.org/mathscinet/pdf/2102853.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:02126475&type=pdf&format=complete},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/LPSemantics.pdf},
abstract = {A new semantics is presented for the logic of proofs~($\mathbf{LP}$), (\cite{Art95TR}, \cite{Art01BSL})
based on the intuition that it is a logic of explicit knowledge.
This semantics is used to give new proofs of several basic results concerning~$\mathbf{LP}$.
In particular, the realization of~$\mathbf{S4}$ into~$\mathbf{LP}$ is established in a way
that carefully examines and explicates the role of the $+$~operator.
Finally connections are made with the conventional approach, via soundness and completeness results.}
}
@incollection{Fit05LY,
author = {Melvin Fitting},
title = {A Logic of Explicit Knowledge},
booktitle = {Logica Yearbook 2004},
publisher = {Filosofia},
address = {Prague},
year = {2005},
editor = {Libor B{\v{e}}hounek and Marta B{\'i}lkov{\'a}},
pages = {11--22},
conference = {http://logika.flu.cas.cz/redaction.php?action=showRedaction&id_categoryNode=1058},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/ExplicitKnow.pdf},
pubweb = {http://logika.flu.cas.cz/redaction.php?action=showRedaction&id_categoryNode=1090},
abstract = {A well-known problem with Hintikka-style logics of knowledge is that of logical omniscience.
One knows too much.
This breaks down into two subproblems: one knows all tautologies, and one’s knowledge is closed under consequence.
A way of addressing the second of these is to move from knowledge simpliciter, to knowledge for a reason.
Then, as consequences become `further away' from one’s basic knowledge, reasons for them become more complex,
thus providing a kind of resource measurement.
One kind of reason is a formal proof.
Sergei Artemov has introduced a logic of explicit proofs,~$\mathbf{LP}$.
I present a semantics for this, based on the idea that it is a logic of knowledge with explicit reasons.
A number of fundamental facts about~$\mathbf{LP}$ can be established using this semantics.
But it is equally important to realize that it provides a natural logic of more general applicability than
its original provenance, arithmetic provability.}
}
@inproceedings{Fit05PLS,
author = {Melvin Fitting},
title = {A Quantified Logic of Explicit Evidence},
booktitle = {Proceedings of the 5th~{P}anhellenic {L}ogic {S}ymposium},
year = {2005},
month = jul # { 25--28,},
address = {Athens, Greece},
publisher = {University of {A}thens},
pages = {6},
note = {Abstract of invited talk},
conference = {http://cgi.di.uoa.gr/~pls5/},
pdf = {http://www.softlab.ntua.gr/~nickie/tmp/pls5/abstracts.pdf#page=6},
abstract = {G{\"{o}}del suggested the creation of a propositional logic of explicit proofs,
and recently this suggestion was carried out by Artemov, to produce the logic~$\mathsf{LP}$.
This logic can, in fact, be looked at more generally as a logic of explicit evidence.
A major result about~$\mathsf{LP}$ is the Realization Theorem,
that says any theorem of~$\mathsf{S4}$ can be converted into a theorem of~$\mathsf{LP}$
by some replacement of necessitation symbols with explicit proof terms.
Thus the necessitation operator of~$\mathsf{S4}$ can be seen as a kind of implicit existential quantifier:
there exists explicit evidence such that....
I introduce quantification over evidence into~$\mathsf{LP}$,
and show that the connection between~$\mathsf{S4}$ necessitation and the existential quantifier is an explicit one.
The extension of~$\mathsf{LP}$ with quantifiers is called~$\mathsf{QLP}$.
I will sketch its semantics and axiomatization.}
}
@incollection{Fit06WoLLIC,
author = {Melvin Fitting},
title = {A Quantified Logic of Evidence},
booktitle = {Proceedings of the 12th {W}orkshop on {L}ogic, {L}anguage, {I}nformation and {C}omputation
({WoLLIC} 2005),
Florian{\'{o}}polis, {S}anta {C}atarina, {B}razil, 19--22 {J}uly 2005},
year = {2006},
editor = {R[uy] de Queiroz and A. Macintyre and G. Bittencourt},
volume = {143},
series = {Electronic Notes in Theoretical Computer Science},
pages = {59--71},
month = jan,
publisher = {Elsevier},
note = {Journal version published as~\cite{Fit08APAL}},
conference = {http://www.cin.ufpe.br/~wollic/wollic2005/},
slides = {http://www.cin.ufpe.br/~wollic/wollic2005/Brazil_Tutorial_2005.pdf},
doi = {10.1016/j.entcs.2005.04.038},
keywords = {logic of knowledge, modal logic, Kripke semantics, LP},
abstract = {A propositional logic of explicit proofs,~$\mathsf{LP}$, was introduced in~\cite{Art01BSL},
completing a project begun long ago by G{\"{o}}del,~\cite{Goed38CW}.
$\mathsf{LP}$~can be looked at more generally as a logic of explicit evidence,
something currently being investigated.
The Realization Theorem for~$\mathsf{LP}$ says
that any theorem of~$\mathsf{S4}$ can be converted into a theorem of~$\mathsf{LP}$ by some replacement
of necessitation symbols with explicit proof terms.
Thus $[]$~of~$\mathsf{S4}$ is a kind of implicit existential quantifier:
there exists a proof term (explicit evidence) such that\ldots.
Here, quantification over evidence is added to~$\mathsf{LP}$,
and it is shown that the connection between $\mathsf{S4}$~necessitation and the existential quantifier is direct.
The extension of~$\mathsf{LP}$ with quantifiers is called~$\mathsf{QLP}$.
A semantics and an axiom system for~$\mathsf{QLP}$ are given,
soundness and completeness are established, and several results are proved relating~$\mathsf{QLP}$
to~$\mathsf{LP}$ and to~$\mathsf{S4}$.}
}
@techreport{Fit06TR,
author = {Melvin Fitting},
title = {A Replacement Theorem For {LP}},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2006},
number = {TR--2006002},
month = mar,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=174},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2006002.pdf},
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$ in a formula may be replaced with occurrences of~$B$ to produce a formula equivalent to the original one.
This theorem does not hold for~$\mathsf{LP}$, Logic of Proofs.
A replacement for replacement is not simple to formulate.
In this note I have provided one, along with some machinery for working with $\mathsf{LP}$~realizations
that may prove useful for other things as well.}
}
@techreport{Fit07TRa,
author = {Melvin Fitting},
title = {Realizing Substitution Instances of Modal Theorems},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007006},
month = mar,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=326},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007006.pdf},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2007006.ps},
abstract = {Suppose $X$~is a theorem of~$\mathsf{S4}$, and a realization for~$X$ has been constructed.
If $X'$~is a substitution instance of~$X$, it is also a theorem of~$\mathsf{S4}$,
and so is realizable, but the only available algorithm for producing a realization of~$X'$, so far,
has been to apply a general realization algorithm to a cut-free proof of~$X'$.
In effect we start over and the realization of~$X$ plays no role.
It is the purpose of this report to present an algorithm
for realizing substitution instances of a realizable formula that is, we believe,
more efficient than a simple appeal to a general realization algorithm itself.}
}
@incollection{Fit07LFCS,
author = {Melvin Fitting},
title = {Realizations and {LP}},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2007,
{N}ew {Y}ork, {NY}, {USA}, {J}une~4--7, 2007, Proceedings},
year = {2007},
editor = {Sergei N. Artemov and Anil Nerode},
volume = {4514},
series = {Lecture Notes in Computer Science},
pages = {212--223},
publisher = {Springer},
note = {Journal version published as~\cite{Fit09APAL}},
doi = {10.1007/978-3-540-72734-7_15},
conference = {http://lfcs.info/lfcs07/},
abstract = {$\mathsf{LP}$~can be seen as a logic of knowledge with justifications.
Artemov's Realization Theorem says justifications can be extracted from validities
in the Hintikka-style logic of knowledge~$\mathsf{S4}$, where they are not explicitly present.
We provide tools for reasoning about justifications directly.
Among other things, we provide machinery for combining two realizations of the same formula,
and for replacing subformulas by equivalent subformulas.
The results are algorithmic in nature---semantics for~$\mathsf{LP}$ plays no role.
We apply our results to provide a new algorithmic proof of Artemov's Realization Theorem itself.}
}
@techreport{Fit07TRb,
author = {Melvin Fitting},
title = {Justification Logics and Conservative Extensions},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007015},
month = jul,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=339},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007015.pdf},
note = {Later versions published as conference presentation~\cite{Fit08ISAIM} and journal version~\cite{Fit08AMAI}},
abstract = {Several justification logics have evolved, starting with the logic~$\mathsf{LP}$,~\cite{Art01BSL}.
These can be thought of as explicit versions of modal logics, or logics of knowledge or belief
in which the unanalyzed necessity operator has been replaced with a family of explicit justification terms.
Modal logics come in various strengths.
For their corresponding justification logics, differing strength is reflected in different vocabularies.
What we show here is that for justification logics corresponding to modal logics extending~$\mathsf{T}$,
extensions are actually conservative.
Our method of proof is very simple, and general enough to also handle several justification logics
not directly corresponding to modal logics.
Our methods do not, however, allow us to prove comparable results for justification logics
corresponding to modal logics that do not extend~$\mathsf{T}$.
That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief.
This remains open.}
}
@techreport{Fit07TRc,
author = {Melvin Fitting},
title = {{S4LP} and Local Realizability},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007020},
month = nov,
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007020.pdf},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=344},
note = {Later version published as~\cite{Fit08CSR}},
abstract = {The logic~$\mathsf{S4LP}$ combines the modal logic~$\mathsf{S4}$ with the justification logic~$\mathsf{LP}$.
This is the case both axiomatically and semantically, though of course the real story is in the details.
We introduce a simple restriction on the behavior of constants in~$\mathsf{S4LP}$,
a restriction that has no effect on the $\mathsf{LP}$~sublogic.
With this assumed, some very powerful derived rules are established.
Then these are used to show we have completeness relative to a semantics having
what we call the \emph{local realizability} property.
This means that at each world of such a model, for each formula true at that world
there is a realization also true at that world,
where a realization is the result of replacing all modal operators with explicit justification terms.
This is part of a attempt to understand the deeper aspects of Artemov's Realization Theorem,
though it is not yet clear just how the results obtained here relate to that theorem.}
}
@inproceedings{Fit08ISAIM,
author = {Melving Fitting},
title = {Explicit Logics of Knowledge and Conservativity},
booktitle = {Online Proceedings of Tenth International Symposium on Artificial Intelligence and Mathematics ({ISAIM} 2008)},
year = {2008},
month = jan # { 2--4,},
address = {{F}ort {L}auderdale, {F}lorida, USA},
note = {Journal version published as~\cite{Fit08AMAI}},
conference = {http://isaim2008.unl.edu/},
pdf = {http://isaim2008.unl.edu/PAPERS/SS1-AI+Logic/MFitting-ss1.pdf},
abstract = {Several justification logics have evolved, starting with the logic~$\mathsf{LP}$,~\cite{Art01BSL}.
These can be thought of as explicit versions of modal logics, or logics of knowledge or belief,
in which the unanalyzed necessity (knowledge, belief) operator has been replaced
with a family of explicit justification terms.
Modal logics come in various strengths.
For their corresponding justification logics, differing strength is reflected in different vocabularies.
What we show here is that for justification logics corresponding to modal logics extending~$\mathsf{T}$,
various familiar extensions are actually conservative with respect to each other.
Our method of proof is very simple, and general enough to handle several justification logics
not directly corresponding to distinct modal logics.
Our methods do not, however, allow us to prove comparable results for justification logics
corresponding to modal logics that do not extend~$\mathsf{T}$.
That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief.
This remains open.}
}
@article{Fit08APAL,
author = {Melvin Fitting},
title = {A quantified logic of evidence},
journal = {Annals of Pure and Applied Logic},
year = {2008},
volume = {152},
number = {1--3},
pages = {67--83},
month = mar,
doi = {10.1016/j.apal.2007.11.003},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/QLP.pdf},
review = {http://www.ams.org/mathscinet/pdf/2397490.pdf},
keywords = {logic of proofs, justification logic, logic of knowledge, modal logic, realization theorem},
abstract = {A propositional logic of explicit proofs,~$\mathsf{LP}$, was introduced in~\cite{Art01BSL},
completing a project begun long ago by G{\"{o}}del,~\cite{Goed38CW}.
$\mathsf{LP}$~can be looked at in a more general way, as a logic of explicit evidence,
and there have been several papers along these lines.
A major result about~$\mathsf{LP}$ is the Realization Theorem, that says
any theorem of~$\mathsf{S4}$ can be converted into a theorem of~$\mathsf{LP}$ by some replacement
of necessitation symbols with explicit proof terms.
Thus the necessitation operator of~$\mathsf{S4}$ can be seen as a kind of implicit existential quantifier:
there exists a proof term (explicit evidence) such that\ldots.
In this paper, quantification over evidence is introduced into~$\mathsf{LP}$,
and it is shown that the connection between $\mathsf{S4}$~necessitation and the existential quantifier
becomes an explicit one.
The extension of~$\mathsf{LP}$ with quantifiers is called~$\mathsf{QLP}$.
A semantics and an axiom system for~$\mathsf{QLP}$ are given,
soundness and completeness are established, and several results are proved relating~$\mathsf{QLP}$
to~$\mathsf{LP}$ and to~$\mathsf{S4}$.}
}
@incollection{Fit08CSR,
author = {Melvin Fitting},
title = {{S4LP} and Local Realizability},
booktitle = {Computer Science~--- Theory and Applications, Third International {C}omputer {S}cience Symposium in {R}ussia, {CSR~2008},
{M}oscow, {R}ussia, {J}une 7--12, 2008, Proceedings},
year = {2008},
editor = {Edward A. Hirsch and Alexander A. Razborov and Alexei Semenov and Anatol Slissenko},
volume = {5010},
series = {Lecture Notes in Computer Science},
pages = {168--179},
publisher = {Springer},
doi = {10.1007/978-3-540-79709-8_19},
conference = {http://csr2008.ru/},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/S4LPLocalRealiz.pdf},
abstract = {The logic~$\mathsf{S4LP}$ combines the modal logic~$\mathsf{S4}$ with the justification logic~$\mathsf{LP}$,
both axiomatically and semantically.
We introduce a simple restriction on the behavior of constants in~$\mathsf{S4LP}$,
having no effect on the $\mathsf{LP}$~sublogic.
Under this restriction some powerful derived rules are established.
Then these are used to show completeness relative to a semantics having
what we call the \emph{local realizability} property:
at each world and for each formula true at that world
there is a realization also true at that world,
where a realization is the result of replacing all modal operators with explicit justification terms.
This is part of a project to understand the deeper aspects of Artemov's Realization Theorem.}
}
@article{Fit08AMAI,
author = {Melvin Fitting},
title = {Justification logics, logics of knowledge, and conservativity},
journal = {Annals of Mathematics and Artificial Intelligence},
year = {2008},
volume = {53},
number = {1--4},
pages = {153--167},
month = aug,
doi = {10.1007/s10472-009-9112-2},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/justconserv.pdf},
keywords = {logic, modal logic, logic of knowledge, justification logic, conservativity},
abstract = {Several \emph{justification logics} have been created, starting with the logic~$\mathsf{LP}$,~(\cite{Art01BSL}).
These can be thought of as explicit versions of modal logics, or of logics of knowledge or belief,
in which the unanalyzed necessity (knowledge, belief) operator has been replaced with a family of explicit justification terms.
We begin by sketching the basics of justification logics and their relations with modal logics.
Then we move to new material.
Modal logics come in various strengths.
For their corresponding justification logics, differing strength is reflected in different vocabularies.
What we show here is that for justification logics corresponding to modal logics extending~$\mathsf{T}$,
various familiar extensions are actually conservative with respect to each other.
Our method of proof is very simple, and general enough to handle several justification logics not directly corresponding to distinct modal logics.
Our methods do not, however, allow us to prove comparable results for justification logics corresponding to modal logics that do not extend~$\mathsf{T}$.
That is, we are able to handle explicit logics of knowledge, but not explicit logics of belief. This remains open.}
}
@unpublished{Fit08Unp,
author = {Melvin Fitting},
title = {Possible World Semantics for First Order~$\mathsf{LP}$},
note = {Work in progress},
year = {2008},
month = nov,
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/FOLP.pdf}
}
@incollection{Fit09TL,
author = {Melvin Fitting},
title = {Reasoning with Justifications},
booktitle = {Towards Mathematical Philosophy, Papers from the {S}tudia {L}ogica conference {T}rends in {L}ogic{~IV}},
publisher = {Springer},
volume = {28},
year = {2009},
editor = {David Makinson and Jacek Malinowski and Heinrich Wansing},
series = {Trends in Logic},
chapter = {6},
pages = {107--123},
conference = {http://www.logika.umk.pl/TrendsIV.html},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/ReasoningJustifications.pdf},
doi = {10.1007/978-1-4020-9084-4_6},
keywords = {logic of knowledge, justification logic, modal logic},
note = {Published online November~2008},
abstract = {This is an expository paper in which the basic ideas of a family of \emph{Justification Logics} are presented.
Justification Logics evolved from a logic called~$\mathsf{LP}$,
introduced by Sergei Artemov~\cite{Art95TR}, \cite{Art01BSL},
which formed the central part of a project to provide an arithmetic semantics for propositional intuitionistic logic.
The project was successful, but there was a considerable bonus:
$\mathsf{LP}$~came to be understood as a logic of knowledge with explicit justifications and,
as such, was capable of addressing in a natural way long-standing problems of logical omniscience.
Since then,$\mathsf{LP}$~has become one member of a family of related logics,
all logics of knowledge with explicit knowledge terms.
In this paper the original problem of intuitionistic foundations is discussed only briefly.
We concentrate entirely on issues of reasoning about knowledge.}
}
@inproceedings{Fit09Ind,
author = {Melvin Fitting},
title = {The Realization Theorem for~{$\mathsf{S5}$}, a Simple, Constructive Proof},
booktitle = {Proceedings of the {S}econd {I}ndian Conference on Logic and Its Relationship with Other Disciplines},
year = {2009},
editor = {A. Gupta and van Benthem, J.},
note = {Forthcoming},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/ForRohit.pdf},
abstract = {Justification logics are logics of knowledge in which explicit reasons are formally represented.
Standard logics of knowledge have justification logic analogs.
Connecting justification logics and logics of knowledge are Realization Theorems.
In this paper we give a new, constructive proof of the Realization Theorem connecting~$\mathsf{S5}$
and its justification analog,~$\mathsf{JS5}$.
This proof is, I believe, the simplest in the literature.}
}
@article{Fit09APAL,
author = {Melvin Fitting},
title = {Realizations and {LP}},
journal = {Annals of Pure and Applied Logic},
year = {2009},
volume = {161},
number = {3},
pages = {368--387},
month = dec,
note = {Published online August~2009},
keywords = {logic of proofs, justification logic, logic of knowledge, modal logic, realization theorem},
doi = {10.1016/j.apal.2009.07.010},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/RealizeTheorem.pdf},
abstract = {$\mathsf{LP}$~can be seen as a logic of knowledge with justifications.
See~\cite{Art08RSL} for a recent comprehensive survey of justification logics generally.
Artemov's Realization Theorem says justifications can be extracted from validities
in the more conventional Hintikka-style logic of knowledge~$\mathsf{S4}$,
in which they are not explicitly present.
Justifications, however, are far from unique.
There are many ways of realizing each theorem of~$\mathsf{S4}$ in the logic~$\mathsf{LP}$.
If the machinery of justifications is to be applied to artificial intelligence, or better yet,
to everyday reasoning, we will need to work with whatever justifications we may have at hand---one
version may not be interchangeable with another, even though they realize the same $\mathsf{S4}$~formula.
In this paper we begin the process of providing tools for reasoning about justifications directly.
The tools are somewhat complex, but in retrospect this should not be surprising.
Among other things, we provide machinery for combining two realizations of the same formula,
and for replacing subformulas by equivalent subformulas.
(The second of these is actually weaker than just stated, but this is not the place for a detailed formulation.)
The results are algorithmic in nature---semantics for~$\mathsf{LP}$ plays no role.
We apply our results to provide a new algorithmic proof of Artemov's Realization Theorem itself.
This paper is a much extended version of~\cite{Fit07LFCS}.}
}
@article{Fit10JAL,
author = {Melvin Fitting},
title = {Justification Logics and Hybrid Logics},
journal = {Journal of Applied Logic},
year = {2010},
volume = {8},
number = {4},
pages = {356--370},
month = dec,
note = {Published online August~2010},
keywords = {hybrid logic, justification logic, logic of proofs, nominals},
doi = {10.1016/j.jal.2010.08.007},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/HybridJustification.pdf},
abstract = {Hybrid logics internalize their own semantics.
Members of the newer family of justification logics internalize their own proof methodology.
It is an appealing goal to combine these two ideas into a single system,
and in this paper we make a start.
We present a hybrid/justification version of the modal logic~$\mathsf{T}$.
We give a semantics, a proof theory,
and prove a completeness theorem.
In addition, we prove a \emph{Realization Theorem},
something that plays a central role for justification logics generally.
Since justification logics are newer and less well known than hybrid logics,
we sketch their background,
and give pointers to their range of applicability.
We conclude with suggestions for future research.
Indeed, the main goal of this paper is to encourage others to continue the investigation begun here.}
}
@unpublished{Fit11Unp,
author = {Melvin Fitting},
title = {Prefixed Tableaus and Nested Sequents},
note = {Submitted},
year = {2011},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/PrefixedDeep6.pdf},
abstract = {Nested sequent systems for modal logics are a relatively recent development,
within the general area known as deep reasoning.
The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator.
Prefixed tableaus go back to~1972,
and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way.
We show that modal nested sequents and prefixed modal tableaus are notational variants of each other,
roughly in the same way that tableaus and Gentzen sequent calculi are notational variants.
This immediately gives rise to new modal nested sequent systems which may be of independent interest.
We discuss some of these, including those for some justification logics that include standard modal operators.}
}
@inbook{GabMak05book,
author = {Dov M. Gabbay and Larisa Maksimova},
title = {Interpolation and Definability: Modal and Intuitionistic Logic},
chapter = {1.3},
pages = {25--34},
publisher = {Clarendon Press},
address = {Oxford},
year = {2005},
volume = {46},
series = {Oxford Logic Guides},
doi = {10.1093/acprof:oso/9780198511748.003.0001}
}
@inproceedings{Gha10ESSLLI,
author = {Meghdad Ghari},
title = {Justification Counterpart of Distributed Knowledge Systems},
booktitle = {Proceedings of the $15^\textup{th}$ Student Session
of 13th {E}uropean {S}ummer {S}chool for {L}ogic, {L}anguage and {I}nformation},
year = {2010},
month = aug # {~9--20,},
address = {{C}openhagen, {D}enmark},
editor = {Marija Slavkovik},
organization = {{FoLLI}},
pages = {25--36},
note = {Errata to the paper prepared by the author in February 2011 can be found below.},
pdf = {http://marija.gforge.uni.lu/proceedings.pdf#page=29},
errata = {http://sites.google.com/site/kuznets/justificationlogicbibliography/Ghari10ESSLLI_errata.pdf},
abstract = {In this paper, we will introduce justification counterparts for some distributed knowledge systems.
Our justified systems have explicit knowledge operators of the form~$[[t]]_i F$ and~$[[t]]_{\mathcal{D}} F$,
which are interpreted respectively as ``$t$~is a justification that agent~$i$ accepts for~$F$'',
and ``$t$~is a justification that all agents implicitly accept for~$F$''.
We then present Kripke style models, called pseudo-Fitting, and prove the completeness theorem.
Finally, using labelled sequent calculus of distributed knowledge systems and the fully explanatory property of pseudo-Fitting models,
we establish the realization theorem.}
}
@incollection{Goed38CW,
author = {Kurt G{\"{o}}del},
title = {Vortrag bei {Z}ilsel/{L}ecture at {Z}ilsel's (*1938a)},
booktitle = {Unpublished essays and lectures},
publisher = {Oxford University Press},
year = {1995},
editor = {Solomon Feferman and Dawson, Jr., John W. and Warren Goldfarb and Charles Parsons and Robert M. Solovay},
volume = {III},
series = {{K}urt {G\"{o}}del Collected Works},
pages = {86--113},
pubweb = {http://www.oup.com/uk/catalogue/?ci=9780195147223}
}
@techreport{Gor05TR,
author = {Evan Goris},
title = {Logic of {P}roofs for bounded arithmetic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2005},
number = {TR--2005011},
month = oct,
note = {Later versions published as conference presentation~\cite{Gor06CSR} and journal version~\cite{Gor08TOCS}},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=164},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2005011.ps},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005011.pdf},
abstract = {The logic of proofs is known to be complete for the semantics of proofs in~$\mathsf{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' bounded arithmetic~$\mathsf{S}_2^1$.}
}
@techreport{Gor06TR,
author = {Evan Goris},
title = {Explicit Proofs in Formal Provability Logic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2006},
number = {TR--2006003},
month = mar,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=173},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2006003.ps},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2006003.pdf},
note = {Later version published as~\cite{Gor07LFCS}},
abstract = {In this paper we answer the question what implicit proof assertions in the provability logic~$\mathsf{GL}$
can be realized by explicit proof terms.
In particular we show that the fragment of~$\mathsf{GL}$
which can be realized by generalized proof terms of~$\mathsf{GLA}$ is exactly
the intersection of~$\mathsf{S4}$ and $\mathsf{GL}$
and equals the fragment that can be realized by proof-terms of~$\mathsf{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~$\mathsf{GLA}$
and give an axiomatization for the intersection of~$\mathsf{GL}$ and~$\mathsf{S4}$.}
}
@incollection{Gor06CSR,
author = {Evan Goris},
title = {Logic of {P}roofs for Bounded Arithmetic},
booktitle = {Computer Science~--- Theory and Applications, First International {C}omputer {S}cience Symposium in {R}ussia, {CSR~2006},
{St.~P}etersburg, {R}ussia, {J}une 8--12, 2006, Proceedings},
year = {2006},
editor = {Dima Grigoriev and John Harrison and Edward A. Hirsch},
volume = {3967},
series = {Lecture Notes in Computer Science},
pages = {191--201},
publisher = {Springer},
note = {Journal version published as~\cite{Gor08TOCS}},
doi = {10.1007/11753728_21},
conference = {http://logic.pdmi.ras.ru/~csr2006/},
abstract = {The logic of proofs is known to be complete for the semantics of proofs in Peano Arithmetic~$\mathsf{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’ bounded arithmetic~$\mathsf{S}_2^1$.
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.}
}
@techreport{Gor07TR,
author = {Evan Goris},
title = {Interpreting Knowledge into Belief in the Presence of Negative Introspection},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007005},
month = mar,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=325},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007005.pdf},
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~$\mathsf{S5}$
as the logic of knowledge are determined.
And all the normal modal logics of belief that give rise to~$\mathsf{S4w5}$
as the logic of knowledge are determined.
Among the latter $\mathsf{KD45}$~shows up as a maximal such logic.}
}
@incollection{Gor07LFCS,
author = {Evan Goris},
title = {Explicit Proofs in Formal Provability Logic},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2007,
{N}ew {Y}ork, {NY}, {USA}, {J}une~4--7, 2007, Proceedings},
year = {2007},
editor = {Sergei N. Artemov and Anil Nerode},
volume = {4514},
series = {Lecture Notes in Computer Science},
pages = {241--253},
publisher = {Springer},
doi = {10.1007/978-3-540-72734-7_17},
conference = {http://lfcs.info/lfcs07/},
abstract = {In this paper we answer the question what implicit proof assertions in the provability logic~$\mathsf{GL}$
can be realized by explicit proof terms.
In particular we show that the fragment of~$\mathsf{GL}$
which can be realized by generalized proof terms of~$\mathsf{GLA}$ is exactly
the intersection of~$\mathsf{S4}$ and $\mathsf{GL}$
and equals the fragment that can be realized by proof-terms of~$\mathsf{LP}$.
In the final section of this paper we establish the disjunction property for~$\mathsf{GLA}$
and give an axiomatization for the intersection of~$\mathsf{GL}$ and~$\mathsf{S4}$.}
}
@article{Gor08TOCS,
author = {Evan Goris},
title = {Feasible Operations on Proofs: The {L}ogic of {P}roofs for Bounded Arithmetic},
journal = {Theory of Computing Systems},
year = {2008},
volume = {43},
number = {2},
pages = {185--203},
month = aug,
doi = {10.1007/s00224-007-9058-x},
note = {Published online October~2007},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:05288692&type=pdf&format=complete},
keywords = {logic of proofs, bounded arithmetic},
abstract = {This paper presents a semantics for the logic of proofs~$\mathsf{LP}$
in which all the operations on proofs are realized by feasibly computable functions.
More precisely, we will show that the completeness of~$\mathsf{LP}$ for the semantics of proofs
of Peano Arithmetic extends to the semantics of proofs in Buss' bounded arithmetic~$\mathsf{S}_2^1$.
In view of applications in epistemology of~$\mathsf{LP}$ in particular and
justification logics in general this result shows that explicit knowledge
in the propositional framework can be made computationally feasible.}
}
@article{Gor09APAL,
author = {Evan Goris},
title = {A modal provability logic of explicit and implicit proofs},
journal = {Annals of Pure and Applied Logic},
year = {2009},
volume = {161},
number = {3},
pages = {388--403},
month = dec,
note = {Published online August~2009},
keywords = {justification logic, provability logic, realization theorem},
doi = {10.1016/j.apal.2009.07.020},
abstract = {We establish the bi-modal forgetful projection of the Logic of Proofs and Formal Provability~$\mathsf{GLA}$.
That is to say, we present a normal bi-modal provability logic with modalities~$[]$ and~$[\times]$
whose theorems are precisely those formulas for which the implicit provability assertions represented by the $[\times]$~modality can be realized by explicit proof terms.}
}
@inproceedings{HalPuc07TARK,
author = {Joseph Y. Halpern and Riccardo Pucella},
title = {Dealing With Logical Omniscience},
booktitle = {Theoretical {A}spects of {R}ationality and {K}nowledge, Proceedings of the {XI}th conference ({TARK~2007})},
year = {2007},
editor = {Dov Samet},
pages = {169--176},
address = {{B}russels, {B}elgium},
month = jun # { 25--27,},
publisher = {ACM},
doi = {10.1145/1324249.1324273},
conference = {http://www.info.fundp.ac.be/~pys/TARK07/},
pdf = {http://www.tark.org/proceedings/tark_jun25_07/p169-halpern.pdf},
abstract = {We examine four approaches for dealing with the logical omniscience problem and
their potential applicability:
the syntactic approach, awareness, algorithmic knowledge, and impossible possible worlds.
Although in some settings these approaches are equi-expressive and can capture all epistemic states,
in other settings of interest they are not.
In particular, adding probabilities to the language allows for finer distinctions between different approaches.}
}
@inproceedings{Iem06ASL,
author = {Rosalie Iemhoff},
title = {Basic intuitionistic logic of proofs},
booktitle = {2005 Annual Meeting of the Association for Symbolic Logic,
{S}tanford {U}niversity, {S}tanford, {CA}, {M}arch 19--22, 2005},
year = {2006},
volume = {12(1)},
series = {Bulletin of Symbolic Logic},
pages = {154},
month = mar,
publisher = {Association for Symbolic Logic},
conference = {http://www.stanford.edu/~sommer/ASL.html},
doi = {10.2178/bsl/1140640947},
jstor = {http://www.jstor.org/stable/3515895},
note = {Abstract},
ps = {http://www.math.ucla.edu/~asl/bsl/1201/1201-006.ps},
abstract = {The basic logic of proofs consists of the propositional schemes
that are valid about the proof predicate~$\mathrm{Prf}(x, y)$.
It is a logic in the language of propositional logic extended by expressions~$t:A$,
where $t$~is an atom and $A$~a formula, that are interpreted as ``$t$~is a proof of~$A$''.
We will present an arithmetical completeness theorem for the basic intuitionistic logic of proofs,
that is a completeness theorem w.r.t.~Heyting Arithmetic.
This result disproves the conjecture that the intuitionistic logic of proofs consists
of intuitionistic logic extended by the characteristic axioms of the classical logic of proofs
and the law of excluded middle for expressions~$t:A$.
We will briefly comment on the extension of the result to the case in which functions
on proof terms are allowed.
This is joint work with Sergei Artemov.}
}
@incollection{JapdeJon98HPT,
author = {Giorgi Japaridze and Dick de Jongh},
title = {The Logic of Provability},
booktitle = {Handbook of Proof Theory},
publisher = {Elsevier},
year = {1998},
editor = {Samuel R. Buss},
volume = {137},
series = {Studies in Logic and the Foundations of Mathematics},
type = {Chapter},
chapter = {{VII}},
pages = {475--546},
doi = {10.1016/S0049-237X(98)80022-0},
pdf = {http://www.csc.villanova.edu/~japaridz/Text/prov.pdf}
}
@mastersthesis{Kaz99MT,
author = {E. L. Kazakov},
title = {Logics of Proofs for {S5}},
school = {Lomonosov Moscow State University, Faculty of Mechanics and Mathematics},
year = {1999},
note = {In Russian},
russian = {http://www.mpi-inf.mpg.de/~ykazakov/publications/Diploma.pdf}
}
@techreport{NKru03TR,
author = {Nikolai V. Krupski},
title = {On the Complexity of the Reflected Logic of Proofs},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2003},
number = {TR--2003007},
month = may,
note = {Later version published as~\cite{NKru06TCS}},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=81},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2003007.ps},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2003007.pdf},
keywords = {proof theory, explicit modal logic, logic of proofs, proof polynomials, symbolic models, disjunctive property, complexity},
abstract = {Artemov's system~$\mathcal{LP}$ captures all propositional invariant properties
of a proof predicate ``$x$~proves~$y$''~(\cite{Art95TR}, \cite{Art01BSL}).
Kuznets in~\cite{Kuz00CSL} showed that the satisfiability problem for~$\mathcal{LP}$
belongs to the class~$\Pi_2^p$ of the polynomial hierarchy.
No nontrivial lower complexity bound for~$\mathcal{LP}$ is known.
We describe quite expressive syntactical fragment of~$\mathcal{LP}$ which belongs to~\emph{NP}.
It is~$r\mathcal{LP}_{\land ,\lor}$~-- the set of all theorems of~$\mathcal{LP}$
which are monotone boolean combinations of quasiatomic formulas
(facts of sort ``$t$~proves~$F$'').
A new decision algorithm for this fragment is proposed.
It is based on a new simple independent formalization for~$r\mathcal{LP}$
(the reflected fragment of~$\mathcal{LP}$) and involves the corresponding proof search procedure.
Essentially $r\mathcal{LP}$~contains all the theorems of~$\mathcal{LP}$
supplied with additional information about their proofs.
We show that in many respects $r\mathcal{LP}$~is simpler than~$\mathcal{LP}$ itself.
This gives the complexity bound~(\emph{NP}) for $r\mathcal{LP}$.
In addition we prove a suitable variant of the disjunctive property which extends this bound to~$r\mathcal{LP}_{\land ,\lor}$.}
}
@techreport{NKru05TR,
author = {Nikolai [V.] Krupski},
title = {Typing in Reflective Combinatory Logic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2005},
number = {TR--2005013},
month = oct,
note = {Later version is published as~\cite{NKru06APAL}},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=166},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005013.pdf},
ps = {http://tr.cs.gc.cuny.edu/tr/files/TR-2005013.ps},
abstract = {We study the syntax of Artemov's Reflective Combinatory Logic~$\mathsf{RCL}_{\to}$.
We provide the explicit definition of types for~$\mathsf{RCL}_{\to}$ and
prove that every well-formed term has a unique type.
We establish that the typability testing and detailed type restoration can be done in polynomial time
and that the derivability relation for~$\mathsf{RCL}_{\to}$ is decidable and \emph{PSPACE}-complete.
These results also formalize the intended semantics of the type~$t:F$ in~$\mathsf{RCL}_{\to}$.
Terms~$\mathsf{RCL}_{\to}$ store the complete information about the judgment ``$t$~is a term of type~$F$'',
and this information can be extracted by the type restoration algorithm.}
}
@phdthesis{NKru06PhD,
author = {Nikolai V. Krupski},
title = {On Certain Algorithmic Problems for Formal Systems with Internalization Property},
school = {Lomonosov Moscow State University, Faculty of Mechanics and Mathematics},
year = {2006},
month = apr,
note = {In Russian}
}
@article{NKru06MUMBa,
author = {N[ikolai] V. Krupskii},
title = {Minimal models and complexity of fragments of the logic of proofs},
journal = {Moscow University Mathematics Bulletin},
year = {2006},
volume = {61},
number = {1},
pages = {32--34},
note = {Originally published in Russian},
bl = {http://direct.bl.uk/research/05/07/RN201200622.html},
mathscinet = {http://www.ams.org/mathscinet-getitem?mr=2255056}
}
@article{NKru06MUMBb,
author = {N[ikolai] V. Krupski},
title = {Restoration of types in the reflexive combinatorial logic},
journal = {Moscow University Mathematics Bulletin},
year = {2006},
volume = {61},
number = {3},
pages = {32--34},
note = {Originally published in Russian},
bl = {http://direct.bl.uk/research/41/0A/RN202395336.html}
}
@article{NKru06TCS,
author = {Nikolai V. Krupski},
title = {On the complexity of the reflected logic of proofs},
journal = {Theoretical Computer Science},
year = {2006},
volume = {357},
number = {1--3},
pages = {136--142},
month = jul,
doi = {10.1016/j.tcs.2006.03.015},
keywords = {logic of proofs, proof polynomials, symbolic models, disjunctive property, complexity},
abstract = {Artemov’s propositional logic of proofs~$\mathsf{LP}$ captures all invariant properties of proof predicates
``$t$~is a proof of~$F$'' which are represented in~$\mathsf{LP}$ as formulas $t:F$.
Kuznets in~\cite{Kuz00CSL} showed that the satisfiability problem for~$\mathsf{LP}$
belongs to the class~$\Pi_2^p$ of the polynomial hierarchy.
In this paper we consider the \emph{reflected logic of proofs}, $\mathsf{rLP}$,
consisting of formulas~$t:F$ derivable in~$\mathsf{LP}$.
The system~$\mathsf{rLP}$ is as expressible as~$\mathsf{LP}$ itself,
since every~$F$ derivable in~$\mathsf{LP}$ is represented in~$\mathsf{rLP}$ by~$t:F$
for an appropriate proof term~$t$.
We prove a better upper bound (\emph{NP}) for the decision procedure in~$\mathsf{rLP}$.
In addition we prove the disjunctive property for the original logic of proofs~$\mathsf{LP}$,
thus answering a well-known question in this area.}
}
@article{NKru06APAL,
author = {Nikolai [V.] Krupski},
title = {Typing in reflective combinatory logic},
journal = {Annals of Pure and Applied Logic},
year = {2006},
volume = {141},
number = {1--2},
pages = {243--256},
month = aug,
doi = {10.1016/j.apal.2005.11.004},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:05047227&type=pdf&format=complete},
keywords = {proof theory, reflective combinatory logic, well-formed formula, typing, derivability, complexity, cut elimination},
abstract = {We study Artemov's Reflective Combinatory Logic~$\mathsf{RCL}_{\to}$.
We provide the explicit definition of types for~$\mathsf{RCL}_{\to}$ and
prove that every well-formed term has a unique type.
We establish that the typability testing and detailed type restoration can be done in polynomial time
and that the derivability relation for~$\mathsf{RCL}_{\to}$ is decidable and \emph{PSPACE}-complete.
These results also formalize the intended semantics of the type~$t:F$ in~$\mathsf{RCL}_{\to}$.
Terms~$\mathsf{RCL}_{\to}$ store the complete information about the judgment ``$t$~is a term of type~$F$'',
and this information can be extracted by the type restoration algorithm.}
}
@incollection{VKru97LFCS,
author = {Vladimir N. Krupski},
title = {Operational logic of proofs with functionality condition on proof predicate},
booktitle = {Logical {F}oundations of {C}omputer {S}cience, 4th International Symposium, {LFCS}'97,
{Y}aroslavl, {R}ussia, {J}uly 6--12, 1997, Proceedings},
year = {1997},
editor = {Sergei Adian and Anil Nerode},
volume = {1234},
series = {Lecture Notes in Computer Science},
pages = {167--177},
publisher = {Springer},
doi = {10.1007/3-540-63045-7_18},
ps = {http://lpcs.math.msu.su/~krupski/FLP_LNCS.PS},
abstract = {The extended operational (term-labeled modal) language is used
to give the axiomatic description for functional proof predicate
supplied with effective operations on proofs induced by modus ponens and necessitation rules.
An additional operation is involved which restores a statement from its proof.
The arithmetical completeness and decidability theorems are proved.
The cut-elimination property for Gentzen style reformulation of corresponding logic is established.}
}
@article{VKru99SVIAM,
author = {V[ladimir N.] Krupski},
title = {On proof term representation for {PA}-admissible inference rules},
journal = {Reports of Enlarged Session of the Seminar of {I.} {V}ekua {I}nstitute of Applied Mathematics},
year = {1999},
volume = {14},
number = {4},
pages = {47--48}
}
@article{VKru01APAL,
author = {Vladimir N. Krupski},
title = {The single-conclusion proof logic and inference rules specification},
journal = {Annals of Pure and Applied Logic},
year = {2001},
volume = {113},
number = {1--3},
pages = {181--206},
month = dec,
doi = {10.1016/S0168-0072(01)00058-6},
conference = {http://logic.pdmi.ras.ru/LogicDays},
ps = {http://lpcs.math.msu.su/~krupski/flpapal.ps},
review = {http://www.ams.org/mathscinet/pdf/1875743.pdf},
keywords = {logic of proofs, explicit modal logic, single-conclusion proof predicate, proof term, inference rule specification, admissible rule},
abstract = {The \emph{logic of single-conclusion} (\emph{functional}) \emph{proofs}~($\mathcal{FLP}$) is introduced.
It combines the verification property of proofs with the single valuedness of proof predicate and
describes the operations on proofs induced by modus ponens rule and proof checking.
It is proved that $\mathcal{FLP}$~is decidable, sound and complete with respect to
arithmetical proof interpretations based on single-valued proof predicates.
The application to arithmetical inference rules specification and $\mathcal{PA}$-admissibility testing is considered.
We show that the provability in~$\mathcal{FLP}$ gives the complete admissibility test
for the rules which can be specified by schemes in $\mathcal{FLP}$-language.
The test is supplied with the ground proof extraction algorithm
which eliminates the admissible rules from a $\mathcal{PA}$-proof by utilizing the information
from the corresponding $\mathcal{FLP}$-proofs.}
}
@article{VKru06JLC,
author = {Vladimir N. Krupski},
title = {Reference Constructions in the Single-conclusion Proof Logic},
journal = {Journal of Logic and Computation},
year = {2006},
volume = {16},
number = {5},
pages = {645--661},
month = oct,
doi = {10.1093/logcom/exl028},
conference = {http://www.mccme.ru/ml2005/},
review = {http://www.ams.org/mathscinet/pdf/2269470.pdf},
keywords = {proof theory, explicit modal logic, single conclusion logic of proofs, proof term, reference, unification},
abstract = {We propose an extension of the propositional proof logic language by the second-order variables
denoting the reference constructors (like `the formula which is proven by~$x$').
The proof logic in this weak second-order language is axiomatized via the calculus~$\mathsf{FLP}_{\textit{ref}}$,
the (\emph{Functional}) \emph{Logic of Proofs with References}.
It is supplied with the formal arithmetical semantics: we prove that
$\mathsf{FLP}_{\textit{ref}}$~is sound with respect to arithmetical interpretations and
is a conservative extension of propositional single-conclusion proof logic~$\mathsf{FLP}$.
Finally, we demonstrate how the language of~$\mathsf{FLP}_{\textit{ref}}$ can be used
as a scheme language for arithmetic and provide the corresponding proof conversion method.}
}
@article{VKru06TCS,
author = {Vladimir N. Krupski},
title = {Referential logic of proofs},
journal = {Theoretical Computer Science},
year = {2006},
volume = {357},
number = {1--3},
pages = {143--166},
month = jul,
doi = {10.1016/j.tcs.2006.03.016},
pdf = {http://lpcs.math.msu.su/~krupski/lp_refel2.pdf},
review = {http://www.ams.org/mathscinet/pdf/2242761.pdf},
keywords = {proof theory, explicit modal logic, single conclusion logic of proofs, proof term, reference, unification, admissible inference rule},
abstract = {We introduce an extension of the propositional logic of single-conclusion proofs
by the second-order variables denoting the reference constructors of the type
``the formula which is proved by~$x$.''
The resulting \emph{Logic of Proofs with References},~$\mathsf{FLP}_{\textup{ref}}$,
is shown to be decidable, and to enjoy soundness and completeness
with respect to the intended provability semantics.
We show that $\mathsf{FLP}_{\textup{ref}}$~provides a complete test of admissibility of inference rules
in a sound extension of arithmetic.
This paper may be regarded as a contribution to the theory of automated reasoning systems.}
}
@incollection{VKru10CSR,
author = {Vladimir N. Krupski},
title = {Symbolic Models for Single-Conclusion Proof Logics},
booktitle = {Computer Science --- Theory and Applications, 5th~International {C}omputer {S}cience Symposium in {R}ussia, {CSR~2010},
{K}azan, {R}ussia, {J}une 16--20, 2010, Proceedings},
publisher = {Springer},
year = {2010},
editor = {Farid Ablayev and Ernst W. Mayr},
volume = {6072},
series = {Lecture Notes in Computer Science},
pages = {276--287},
conference = {http://csr2010.antat.ru/},
doi = {10.1007/978-3-642-13182-0_26},
abstract = {Symbolic semantics for logics of proofs based on Mkrtychev models covers the the case of multi-conclusion proof logics.
We propose symbolic models for single-conclusion proof logics ($FLP$~and its extensions).
The corresponding soundness and completeness theorems are proven.
The developed symbolic model technique is used to establish the consistency of contexts required for proof internalization.
In particular, we construct an extension of~$FLP$ that enjoys the strong proof internalization property with empty context.}
}
@incollection{Kur09LFCS,
author = {Hidenori Kurokawa},
title = {Tableaux and Hypersequents for {J}ustification {L}ogic},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2009,
{D}eerfield {B}each, {FL}, {USA}, {J}anuary 3--6, 2009, Proceedings},
publisher = {Springer},
year = {2009},
editor = {Sergei [N.] Artemov and Anil Nerode},
volume = {5407},
series = {Lecture Notes in Computer Science},
pages = {295--308},
conference = {http://lfcs.info/lfcs09/},
doi = {10.1007/978-3-540-92687-0_20},
abstract = {Justification Logic is a new generation of epistemic logics
which along with the traditional modal knowledge/belief operators also consider justification assertions
`$t$~ is a justification for~$F$.'
In this paper, we introduce a prefixed tableau system for one of the major logics of this kind~$\mathsf{S4LPN}$,
which combines the logic of proofs~($\mathsf{LP}$) and epistemic logic~$\mathsf{S4}$
with an explicit negative introspection principle $\neg t:F \to []\neg t:F$.
We show that the prefixed tableau system for~$\mathsf{S4LPN}$ is sound and complete with respect to Fitting-style semantics.
We also introduce a hypersequent calculus~$\mathsf{HS4LPN}$ and show that $\mathsf{HS4LPN}$~is complete as far as we confine ourselves
to a case where only a single formula is to be proven.
We establish this fact by using a translation from the prefixed tableau system to the hypersequent calculus.
This completeness result gives us a semantic proof of cut-admissibility for~$\mathsf{S4LPN}$ under the aforementioned restriction.}
}
@techreport{Kus07TR,
author = {Hirohiko Kushida},
title = {Linear {L}ogic with explicit resources},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007017 },
month = sep,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=341},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007017.pdf},
abstract = {In linear logic, a formula~$!A$ with the modality~$!$ means that
$A$~can be duplicated as many times as we like.
We can paraphrase this as `$A$~holds with an empty resource'.
Then it is natural to generalize formulas with modalities to the form~$s:A$
with a term~$s$, of which meaning is that $A$~holds if there is a resource~$s$.
Terms are interpreted as elements of a well-ordered set;
$!$~is interpreted as the least element.
In this paper, we present an extended system of linear logic with such formulas~$s:A$
as `linear logic with explicit resources'.
We show some basic properties of the logic:
the soundness and completeness theorems with respect to a denotational semantics (Phase semantics),
the cut-elimination theorem (normalization theorem).
In addition, we consider the fragment containing no~$!$ and prove the faithful embeddability of
(ordinary) linear logic in the fragment.}
}
@incollection{Kuz00CSL,
author = {Roman Kuznets},
title = {On the Complexity of Explicit Modal Logics},
booktitle = {{C}omputer {S}cience {L}ogic, 14th~International Workshop,
{CSL}~2000, Annual Conference of the {EACSL},
{F}ischbachau, {G}ermany, {A}ugust~21--26, 2000, Proceedings},
year = {2000},
editor = {Peter G. Clote and Helmut Schwichtenberg},
volume = {1862},
series = {Lecture Notes in Computer Science},
pages = {371--383},
publisher = {Springer},
note = {Errata concerning the explicit counterparts of~$\mathcal{D}$ and~$\mathcal{D}4$ are published as~\cite{Kuz09LC}},
doi = {10.1007/3-540-44622-2_25},
conference = {http://www.tcs.informatik.uni-muenchen.de/csl2000/},
pdf = {http://sites.google.com/site/kuznets/csl2000.pdf},
abstract = {Explicit modal logic was introduced by S.~Artemov.
Whereas the traditional modal logic uses atoms~$[]F$ with a possible semantics ``$F$~is provable'',
the explicit modal logic deals with atoms of form~$t:F$, where $t$~is a \emph{proof polynomial}
denoting a specific proof of a formula~$F$.
Artemov found the explicit modal logic~$\mathcal{LP}$ in this new format and
built an algorithm that recovers explicit proof polynomials corresponding to modalities in every derivation
in K.~G{\"{o}}del's modal provability calculus~$\mathcal{S}4$.
In this paper we study the complexity of~$\mathcal{LP}$ as well as the complexity of explicit counterparts
of the modal logics~$\mathcal{K}$, $\mathcal{D}$, $\mathcal{T}$, $\mathcal{K}4$, $\mathcal{D}4$
found by V.~Brezhnev.
The main result: the satisfiability problem for each of these explicit modal logics belongs to the
class~$\Sigma_2^p$ of the polynomial hierarchy.
Similar problem for the original modal logics is known to be PSPACE-complete.
Therefore, explicit modal logics have much better upper complexity bounds than the original modal logics.}
}
@inproceedings{Kuz05ASL,
author = {Roman Kuznets},
title = {On decidability of the logic of proofs with arbitrary constant specifications},
booktitle = {2004~Annual Meeting of the {A}ssociation for {S}ymbolic {L}ogic,
{C}arnegie {M}ellon {U}niversity, {P}ittsburgh, {PA}, {M}ay~19--23, 2004},
year = {2005},
volume = {11(1)},
series = {Bulletin of Symbolic Logic},
pages = {111},
month = mar,
publisher = {Association for Symbolic Logic},
conference = {http://www.aladdin.cs.cmu.edu/asl/},
jstor = {http://www.jstor.org/stable/3219639},
note = {Abstract},
ps = {http://www.math.ucla.edu/~asl/bsl/1101/1101-005.ps},
euclid = {http://projecteuclid.org/euclid.bsl/1107959501},
abstract = {Logic of Proofs~$\mathcal{LP}$ introduced by Artemov gave an exact intended semantics for
G{\"{o}}del's logic of provability~$\mathcal{S}4$~\cite{Art95TR}, \cite{Art01BSL}.
This Logic of Proofs considers statements of the form~$t:F$
where a proof term~$t$ (called proof polynomial) denotes a proof for~$F$.
Proof polynomials are built from variables and proof constants~$c$
which stand for proofs of axioms of the theory.
Logic of Proofs has a natural arithmetical semantics where $t:F$~is interpreted
as a formal arithmetical statement ``$t$~is a proof of~$F$ in~$\mathcal{PA}$.''
Proof constants are specified by accepting as postulates constant specifications~$\mathcal{CS}$
which are sets of formulas of sort $\{c_1:A_1, c_2:A_2, \ldots\}$
where $c_i$~is a proof constant and $A_i$~an axiom.
A theory~$\mathcal{LP}_{\mathcal{CS}}$ is a theory with constant specification~$\mathcal{CS}$.
Logic~$\mathcal{LP}_0$ corresponding to the empty~$\mathcal{CS}$ was shown to be decidable in~\cite{Art95TR}.
Mkrtychev in~\cite{Mkr97LFCS} has shown that if $\mathcal{CS}$~contains only a finite number of axiom schemes
for each constant then $\mathcal{LP}_{\mathcal{CS}}$~is decidable.
We show that those results do not extend to all decidable constant specifications.
\textbf{Theorem 1}. \emph{There is a decidable constant specification~$\mathcal{CS}$
such that the logic~$\mathcal{LP}_{\mathcal{CS}}$ is undecidable.}
Moreover, it can be shown that even a decidable constant specification involving only one constant
already may lead to an undecidable theory~$\mathcal{LP}_{\mathcal{CS}}$.}
}
@incollection{Kuz06LC,
author = {Roman Kuznets},
title = {Logic of {P}roofs as a measure of {H}ilbert-style proof complexity},
booktitle = {2005~Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'05,
{A}thens, {G}reece, {J}uly~28--{A}ugust~3, 2005},
publisher = {Association for Symbolic Logic},
year = {2006},
volume = {12(2)},
series = {Bulletin of Symbolic Logic},
pages = {355},
month = jun,
note = {Abstract presented by title},
ps = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps},
doi = {10.2178/bsl/1146620064},
abstract = {Logic of Proofs~$\mathsf{LP}$ introduced by Artemov gave an exact intended semantics
for G{\"{o}}del's logic of provability~$\mathsf{S4}$ (see~\cite{Art01BSL}).
This Logic of Proofs considers statements of the form~$t:F$,
where a proof term~$t$ (called proof polynomial) denotes a proof for~$F$.
Logic of Proofs has a natural arithmetical semantics where $t:F$~is interpreted
as a formal arithmetical statement ``$t$~is a proof of~$F$ in~$\mathsf{PA}$.''
We show that the smallest proof polynomial that proves~$F$ can serve as a measure of
how long is the shortest Hilbert-style proof of~$t:F$.
\textbf{Theorem~1.} \emph{Let $t$~be the smallest term such that $\mathsf{LP} \vdash t:F$.
Let $\mathcal{L}_1$ be the shortest Hilbert-style derivation of~$t:F$ in~$\mathsf{LP}$.
Then
\[
\mathit{dag}(t) \leq |\mathcal{L}_1| \leq 3|t|,
\]
where |t|~is the size of the syntactic tree of term~$t$, $\mathit{dag}(t)$~is the size
of the syntactic direct acyclic graph~(dag) of term~$t$, and $|\mathcal{L}_1|$~is the number
of formulas in derivation~$\mathcal{L}_1$.}
We further extend this result to Hilbert-style proofs of propositional tautologies:
\textbf{Theorem~2.} \emph{Let $F$~be a propositional tautology.
Let $t$~be the smallest term such that $\mathsf{LP} \vdash t:F$.
Let $t'$~be the dag-smallest term such that~$\mathsf{LP} \vdash t':F$.
Let $\mathcal{L}_2$~be the shortest Hilbert-style propositional derivation of~$F$. Then
\[
\mathit{dag}(t') \leq |\mathcal{L}_2| = O(|t|).}}
}
@incollection{Kuz06ASLAPA,
author = {Roman Kuznets},
title = {On self-referentiality in modal logic},
booktitle = {2005--06~Winter Meeting of the {A}ssociation for {S}ymbolic {L}ogic,
The {H}ilton {N}ew {Y}ork {H}otel, {N}ew {Y}ork, {NY}, {D}ecember~27--29, 2005},
publisher = {Association for Symbolic Logic},
year = {2006},
volume = {12(3)},
series = {Bulletin of Symbolic Logic},
pages = {510},
month = sep,
note = {Abstract},
doi = {10.2178/bsl/1154698743},
jstor = {http://www.jstor.org/stable/3699489},
ps = {http://www.math.ucla.edu/~asl/bsl/1203/1203-005.ps},
abstract = {One of the applications of modal logic is provability logic with~$[]F$ read as
`formula~$F$ is provable (in a theory~$\mathcal{T}$).'
Another application is epistemology logic where $[]F$~is understood as `formula~$F$ is known
(by an agent~$a$).'
Recently developed logic~$\mathsf{LP}$ (see~\cite{Art01BSL})
provides an explicit version for both applications.
Using $t:F$ to mean `$F$~is provable and $t$~represents its proof' in provability case or
`$F$~is known and $t$~justifies this knowledge' in epistemology case allows for a finer grained discussion.
It was shown~(\cite{Art01BSL}) that $\mathsf{LP}$~is an explicit counterpart of modal logic~$\mathsf{S4}$,
which can be viewed both as an informal provability logic and a logic of knowledge.
In principle, one can imagine a proof or a justification that refers to itself.
For example, it would make sense to reserve one uniform justification for all circular reasoning instances;
such a justification, in particular, would apply to every circular reasoning about this very justification.
The language of modal logic is too poor to capture this notion of self-referentiality.
Its explicit counterpart, on the contrary, can distinguish between self-referential and non-self-referential justifications.
We tried to answer the following question:
Is self-referentiality crucial for the provability/knowledge encompassed by modal logic~$\mathsf{S4}$?
The following theorem affirms that it is.
\textbf{Theorem 1.} Some theorems of~$\mathsf{S4}$ require self-referential proofs
to be given an explicit realization in~$\mathsf{LP}$, e.g.,~$\neg[]\neg(S \to []S)$.}
}
@inproceedings{Kuz06ESSLLI,
author = {Roman Kuznets},
title = {Complexity of Evidence-Based Knowledge},
booktitle = {Proceedings of the
Workshop on {R}ationality and {K}nowledge,
18th~{E}uropean {S}ummer {S}chool in {L}ogic, {L}anguage and {I}nformation ({ESSLLI'}06)},
year = {2006},
organization = {{FoLLI}},
month = aug # { 7--11,},
address = {{M\'{a}}laga, {S}pain},
editor = {Sergei [N.] Artemov and Rohit Parikh},
pages = {66--75},
conference = {http://web.cs.gc.cuny.edu/~sartemov/rkw/},
pdf = {http://sites.google.com/site/kuznets/esslli06.pdf},
proceedings = {http://folli.loria.fr/cds/2006/workshops/Artemov.Parikh.RationalityAndKnowledge.pdf},
abstract = {A system of evidence-based knowledge~$\mathsf{S4LP}$ was recently proposed by Artemov and Nogina.
It combines epistemic modal operator with explicit evidence represented by evidence terms
similar to those of Artemov's Logic of Proofs.
This logic~$\mathsf{S4LP}$ and its generalizations promise a new approach to common-knowledge and
to the logical omniscience problem.
In this paper, we show that this logic is PSPACE-complete.
Thus adding explicit evidence to~$\mathsf{S4}$ does not seem to increase the complexity of the logic.}
}
@incollection{Kuz07LFCS,
author = {Roman Kuznets},
title = {Proof Identity for Classical Logic: Generalizing to Normality},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2007,
{N}ew {Y}ork, {NY}, {USA}, {J}une~4--7, 2007, Proceedings},
year = {2007},
editor = {Sergei N. Artemov and Anil Nerode},
volume = {4514},
series = {Lecture Notes in Computer Science},
pages = {332--348},
publisher = {Springer},
conference = {http://lfcs.info/lfcs07/},
doi = {10.1007/978-3-540-72734-7_24},
pdf = {http://sites.google.com/site/kuznets/LFCS07.pdf},
abstract = {The problem of the identity criteria for proofs can be traced to Hilbert and Prawitz.
One of the approaches, which uses the concept of generality of proofs, was suggested in~1968 by Lambek.
Following his ideas, we propose a language and a logic to represent Hilbert-style proofs
for classical propositional logic by adapting the Logic of Proofs~($\mathsf{LP}$)
introduced by Artemov in~1994.
We prove that proof polynomials, the objects representing Hilbert derivations in~$\mathsf{LP}$,
are sufficient to realize all propositional derivations, with or without hypotheses.
We also show that proof polynomials respect the ideas of generality and provide an algorithm
for determining whether two given proof polynomials represent the same proof.
These results naturally extend similar properties of combinatory logic demonstrated by Hindley.
The language of~$\mathsf{LP}$ allows us to formally capture more structure of Hilbert-style proofs.
In particular, we show how the well-known phenomenon of proof composition in classical logic
manifests itself in the case of Hilbert proofs.}
}
@phdthesis{Kuz08PhD,
author = {Roman Kuznets},
title = {Complexity Issues in Justification Logic},
school = {CUNY Graduate Center},
year = {2008},
month = may,
pdf = {http://sites.google.com/site/kuznets/PhD.pdf},
abstract = {Justification Logic is an emerging field that studies provability, knowledge, and belief
via explicit proofs or justifications that are part of the language.
There exist many justification logics closely related to modal epistemic logics of knowledge and belief.
Instead of modality~$[]$ in pure justification logics, or in addition to modality~$[]$ in hybrid logics,
which has an existential epistemic reading `there exists a proof of~$F$,’
all justification logics use constructs~$t:F$, where a justification term~$t$
represents a blueprint of a Hilbert-style proof of~$F$.
The first justification logic,~$\mathsf{LP}$, introduced by Sergei Artemov,
was shown to be a justification counterpart of modal logic~$\mathsf{S4}$
and serves as a missing link between~$\mathsf{S4}$ and Peano arithmetic,
thereby solving a long-standing problem of provability semantics for~$\mathsf{S4}$ and~$\mathsf{Int}$.
The machinery of explicit justifications can be used to analyze well-known epistemic paradoxes,
e.g. Gettier's examples of justified true belief that can hardly be considered knowledge,
and to find new approaches to the concept of common knowledge.
Yet another possible application is the Logical Omniscience Problem,
which reflects an undesirable property of knowledge as described by modality
when an agent knows all the logical consequences of his/her knowledge.
The language of justification logic opens new ways to tackle this problem.
This thesis focuses on quantitative analysis of justification logics.
We explore their decidability and complexity of Validity Problem for them.
A closer analysis of the realization phenomenon in general and of one procedure in particular
enables us to deduce interesting corollaries about self-referentiality for several modal logics.
A framework for proving decidability of various justification logics is developed
by generalizing the Finite Model Property.
Limitations of the method are demonstrated through an example of an undecidable justification logic.
We study reflected fragments of justification logics and provide them with an axiomatization
and a decision procedure whose complexity (the upper bound) turns out to be uniform
for all justification logics, both pure and hybrid.
For many justification logics, we also present lower and upper complexity bounds.}
}
@incollection{Kuz08CSR,
author = {Roman Kuznets},
title = {Self-referentiality of Justified Knowledge},
booktitle = {Computer Science~--- Theory and Applications, Third International {C}omputer {S}cience Symposium in {R}ussia, {CSR~2008},
{M}oscow, {R}ussia, {J}une 7--12, 2008, Proceedings},
year = {2008},
editor = {Edward A. Hirsch and Alexander A. Razborov and Alexei Semenov and Anatol Slissenko},
volume = {5010},
series = {Lecture Notes in Computer Science},
pages = {228--239},
publisher = {Springer},
conference = {http://csr2008.ru/},
doi = {10.1007/978-3-540-79709-8_24},
pdf = {http://sites.google.com/site/kuznets/CSR08.pdf},
abstract = {The principal result of Justification Logic is the Realization Theorem,
which states that behind major epistemic modal logics there are corresponding systems
of evidence/justification terms sufficient for reading all provable knowledge assertions
as statements about justifications.
A knowledge/belief modality is self-referential if there are modal sentences
that cannot be realized without using self-referential evidence of type
``$t$~is a proof of~$A(t)$.''
Building on an earlier result that S4~and its justification counterpart~$\mathsf{LP}$
describe knowledge that is self-referential,
we show that the same is true for~$\mathsf{K4}$, $\mathsf{D4}$, and~$\mathsf{T}$ with their justification counterparts
whereas for~$\mathsf{K}$ and~$\mathsf{D}$ self-referentiality can be avoided.
Therefore, no single modal axiom from the standard axiomatizations of these logics is
responsible for self-referentiality.}
}
@incollection{Kuz09LC,
author = {Roman Kuznets},
title = {Complexity through tableaux in justification logic},
booktitle = {2008 {E}uropean Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'08,
{B}ern, {S}witzerland, {J}uly~3--{J}uly~8, 2008},
publisher = {Association for Symbolic Logic},
year = {2009},
volume = {15(1)},
series = {Bulletin of Symbolic Logic},
pages = {121},
month = mar,
note = {Abstract},
ps = {http://www.math.ucla.edu/~asl/bsl/1501/1501-005.ps},
doi = {10.2178/bsl/1231081772},
abstract = {Logics~$\mathsf{J}$, $\mathsf{JD}$, $\mathsf{JT}$, $\mathsf{J4}$, $\mathsf{JD4}$, and~$\mathsf{LP}$
are explicit counterparts of modal epistemic logics~$\mathsf{K}$, $\mathsf{D}$, $\mathsf{T}$, $\mathsf{K4}$,
$\mathsf{D4}$, and~$\mathsf{S4}$ respectively (see~\cite{Bre00TR}, \cite{Art07TRb} for more details).
An upper bound of~$\Sigma_2^p$ for the satisfiability problem in these justification logics
was announced in~\cite{Kuz00CSL}.
The algorithm was essentially a propositional tableau procedure (though not presented as such)
followed by a check on possible contradictions among justifications.
The former part is traditionally~NP while the latter was shown to be~co-NP,
thus yielding~$\Sigma_2^p$ as the total complexity.
Recently an omission was found in the proof for two of the six logics: $\mathsf{JD}$ and~$\mathsf{JD4}$.
Restoring the upper bound for~$\mathsf{JD}$ called for the use of prefixed tableaux.
Below we provide the tableau-style formulation of the first part of the original algorithm
for~$\mathsf{J}$, $\mathsf{JT}$, $\mathsf{J4}$, and~$\mathsf{LP}$
as well as a new tableau algorithm for~$\mathsf{JD}$ that help establish the $\Sigma_2^p$~upper bound
for satisfiability problems in all these 5~logics (note the integer prefixes used for~$\mathsf{JD}$).
\[
\mathsf{J}, \mathsf{J4}~~~~~\frac{T s:G}{T *(s,G)}~~~~\frac{F s:G}{F *(s,G)}
\]
\[
\mathsf{JT}, \mathsf{LP}~~~~~\frac{T s:G}{T G \textrm{and} T *(s,G)}~~~~~\frac{F s:G}{F *(s,G)~|~F G}
\]
\[
\mathsf{JD}~~~~~\frac{n T s:G}{n T *(s,G) \textrm{and} n+1 T G}~~~~~\frac{n F s:G}{n F *(s,G)}
\]
Whether the same bound holds for JD4 remains at this point an open problem.}
}
@article{Kuz10TOCS,
author = {Roman Kuznets},
title = {Self-Referential Justifications in Epistemic Logic},
journal = {Theory of Computing Systems},
year = {2010},
volume = {46},
number = {4},
pages = {636--661},
month = may,
note = {Published online April~2009},
abstract = {This paper is devoted to the study of self-referential proofs and/or justifications,
i.e., valid proofs that prove statements about these same proofs.
The goal is to investigate whether such self-referential justifications are present in the reasoning described by standard modal epistemic logics such as~$\mathsf{S4}$.
We argue that the modal language by itself is too coarse to capture this concept of self-referentiality and
that the language of justification logic can serve as an adequate refinement.
We consider well-known modal logics of knowledge/belief and show, using explicit justifications,
that~$\mathsf{S4}$, $\mathsf{D4}$, $\mathsf{K4}$, and~$\mathsf{T}$
with their respective justification counterparts~$\mathsf{LP}$, $\mathsf{JD4}$, $\mathsf{J4}$, and~$\mathsf{JT}$
describe knowledge that is self-referential in some strong sense.
We also demonstrate that self-referentiality can be avoided for~$\mathsf{K}$ and~$\mathsf{D}$.
In order to prove the former result, we develop a machinery of minimal evidence functions used to effectively build models for justification logics.
We observe that the calculus used to construct the minimal functions axiomatizes the reflected fragments of justification logics.
We also discuss difficulties that result from an introduction of negative introspection.},
keywords = {self-referentiality, justification logic, epistemic modal logic, Logic of Proofs},
doi = {10.1007/s00224-009-9209-3},
pdf = {http://sites.google.com/site/kuznets/TOCS09.pdf}
}
@inproceedings{Kuz09PLS,
author = {Roman Kuznets},
title = {A Note on the Use of Sum in the {L}ogic of {P}roofs},
booktitle = {Proceedings of the 7th~{P}anhellenic {L}ogic {S}ymposium},
year = {2009},
month = jul # { 15--19,},
editor = {Costas Drossos and Pavlos Peppas and Constantine Tsinakis},
address = {Patras University, Greece},
publisher = {Patras University Press},
pages = {99--103},
conference = {http://www.bma.upatras.gr/pls7/},
pdf = {http://sites.google.com/site/kuznets/PLS09.pdf},
abstract = {The Logic of Proofs~$\mathsf{LP}$, introduced by Artemov,
encodes the same reasoning as the modal logic~$\mathsf{S4}$
using proofs explicitly present in the language.
In particular, Artemov showed that three operations on proofs (application~$\cdot$, positive introspection~$!$, and sum~$+$)
are sufficient to mimic provability concealed in $\mathsf{S4}$~modality.
While the first two operations go back to G{\"{o}}del, the exact role of~$+$ remained somewhat unclear.
In particular, it was not known whether the other two operations are sufficient by themselves.
We provide a positive answer to this question under a very weak restriction on the axiomatization of~$\mathsf{LP}$.}
}
@incollection{Kuz10PCC,
author = {Roman Kuznets},
title = {A Note on the Abnormality of Realizations {of~$\mathsf{S4LP}$}},
booktitle = {{P}roof, {C}omputation, {C}omplexity {PCC~2010}, International Workshop, Proceedings},
publisher = {Institute of Computer Science and Applied Mathematics, University of Bern},
year = {2010},
editor = {Kai Br{\"u}nnler and Thomas Studer},
number = {IAM--10--001},
series = {{IAM~T}echnical Reports},
month = jun,
conference = {http://pcc2010.unibe.ch/},
pdf = {http://sites.google.com/site/kuznets/pcc10.pdf},
proceedings = {http://www.iam.unibe.ch/de/forschung/publikationen/techreports/2010/iam-10-001/at_download/file},
http = {http://www.iam.unibe.ch/de/forschung/publikationen/techreports/2010/iam-10-001},
note = {Abstract}
}
@techreport{Len09TR,
author = {Florian Lengyel},
title = {Cartesian Closed Categories for the {L}ogic of {P}roofs},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2009},
number = {TR--2009002},
month = mar,
pdf = {http://tr.cs.gc.cuny.edu/tr/files/TR-2009002.pdf},
http = {http://tr.cs.gc.cuny.edu/tr/techreport.php?id=373},
abstract = {A generalization of the Curry-Howard-Lambek isomorphism for Cartesian closed categories and typed lambda calculi is given
for the LP categories with weak natural numbers object,
which correspond to the positive conjunction fragment of the intuitionistic Logic of Proofs~$\textbf{LP}$ of Artemov,
and LP-typed lambda calculi with natural numbers type.}
}
@inproceedings{LetGro11ArgMAS,
author = {Letia, Ioan Alfred and Adrian Groza},
title = {Arguing with Justifications Between Collaborating Agents},
booktitle = {{ArgMAS~2011}, Eighth International Workshop on Argumentation in Multi-Agent Systems,
In conjunction with {AAMAS~2011}, Workshop Proceedings},
year = {2011},
editor = {Peter McBurney and Simon Parsons and Iyad Rahwan},
pages = {44--57},
address = {{T}aipei, {T}aiwan},
month = may,
conference = {http://www.mit.edu/~irahwan/argmas/argmas11/},
pdf = {http://www.cs.huji.ac.il/~jeff/aamas11/workshops/ArgMAS2011.pdf#page=48},
abstract = {We exploit the Justification Logic capabilities of reasoning about justifications,
comparing pieces of evidence,
and measuring the complexity of justifications in the context of argumentative agents.
Not knowing all of the implications of their knowledge base,
agents use justified arguments for reflection and guidance.}
}
@article{LucMon99SL,
author = {Duccio Luchi and Franco Montagna},
title = {An Operational Logic of Proofs with Positive and Negative Information},
journal = {Studia Logica},
year = {1999},
volume = {63},
number = {1},
pages = {7--25},
month = jul,
doi = {10.1023/A:1005298816666},
keywords = {provability logic, logic of proofs, proof theory},
abstract = {The logic of proofs was introduced by Artemov in order to analize the formalization of the concept of proof
rather than the concept of provability.
In this context, some operations on proofs play a very important role.
In this paper, we investigate some very natural operations, paying attention not only to positive information,
but also to negative information (i.e.~information saying that something cannot be a proof).
We give a formalization for a fragment of such a logic of proofs, and we prove that our fragment is complete
and decidable.}
}
@inproceedings{Mil02ASL,
author = {Robert S. Milnikel},
title = {Explicit non-provability and nonmonotonic~{S4}},
booktitle = {2001--2002 {W}inter Meeting of the {A}ssociation for Symbolic Logic,
{S}an {D}iego {M}arriott {H}otel and {M}arina, {S}an {D}iego, {C}alifornia, {J}anuary 8--9, 2002},
year = {2002},
volume = {8(2)},
series = {Bulletin of Symbolic Logic},
pages = {317--318},
month = jun,
publisher = {Association for Symbolic Logic},
doi = {10.2178/bsl/1182353883},
note = {Abstract},
ps = {http://www.math.ucla.edu/~asl/bsl/0802/0802-006.ps},
abstract = {In modal nonmonotonic logics, lack of proof of a formula~$\phi$ is sufficient to conclude~$\neg[]\phi$.
We will make use of explicit modal operators from Artemov's Logic of Proofs~\cite{Art01BSL} to establish non-provability of formulas in~S4.
Our eventual goal is to incorporate the these into sequent proofs for S4~skeptical consequence.}
}
@article{Mil07APAL,
author = {Robert [S.] Milnikel},
title = {Derivability in certain subsystems of the {L}ogic of {P}roofs is {$\Pi^p_2$}-complete},
journal = {Annals of Pure and Applied Logic},
year = {2007},
volume = {145},
number = {3},
pages = {223--239},
month = mar,
doi = {10.1016/j.apal.2006.03.001},
review = {http://www.ams.org/mathscinet/pdf/2286412.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:05126406&type=pdf&format=complete},
keywords = {Logic of Proofs, logic of belief, complexity},
abstract = {The Logic of Proofs realizes the modalities from traditional modal logics with \emph{proof polynomials},
so an expression~$[]F$ becomes~$t:F$ where $t$~is a proof polynomial representing a proof of or evidence for~$F$.
The pioneering work on explicating the modal logic~$\mathcal{S}4$ is due to S.~Artemov and was extended to several subsystems by V.~Brezhnev.
In~2000, R.~Kuznets presented a $\Pi_2^p$~algorithm for deducibility in these logics;
in the present paper we will show that the deducibility problem is $\Pi_2^p$-complete.
(The analogous problem for traditional modal logics is PSPACE-complete.)
Both Kuznets's work and the present results make assumptions on the values of proof constants.}
}
@incollection{Mil09LFCS,
author = {Robert S. Milnikel},
title = {Conservativity for Logics of Justified Belief},
booktitle = {Logical Foundations of Computer Science, International Symposium, {LFCS}~2009,
{D}eerfield {B}each, {FL}, {USA}, {J}anuary 3--6, 2009, Proceedings},
publisher = {Springer},
year = {2009},
editor = {Sergei [N.] Artemov and Anil Nerode},
volume = {5407},
series = {Lecture Notes in Computer Science},
pages = {354--364},
conference = {http://lfcs.info/lfcs09/},
doi = {10.1007/978-3-540-92687-0_24},
abstract = {In~\cite{Fit08ISAIM}, Fitting showed that the standard hierarchy of logics of justified knowledge is conservative
(e.g.~a logic with positive introspection operator~$!$ is conservative over the logic without~$!$).
We do the same with most logics of justified belief,
but taking a semantic approach rather than Fitting's syntactic one.
A brief example shows that conservativity does not hold for logics of justified consistent belief.}
}
@unpublished{Mil09Unp,
author = {Robert S. Milnikel},
title = {Conservativity for Logics of Justified Belief: Two Approaches},
note = {Extended version of~\cite{Mil09LFCS}, submitted to Annals of Pure and Applied Logic},
year = {2009},
month = mar,
pdf = {http://www2.kenyon.edu/Depts/Math/Milnikel/ConservativityAPAL.pdf},
keywords = {justification logic, epistemic logic, logic of belief, proof theory},
abstract = {In~\cite{Fit08ISAIM}, Fitting showed that the standard hierarchy of logics of justified knowledge is conservative
(e.g.~a logic with positive introspection operator~$!$ is conservative over the logic without~$!$).
We do the same with most logics of justified belief,
showing both conservation of sequent proofs and extensibility of models.
A brief example shows that conservativity does not hold for logics of justified consistent belief.}
}
@incollection{Mkr97LFCS,
author = {Alexey Mkrtychev},
title = {Models for the Logic of Proofs},
booktitle = {Logical {F}oundations of {C}omputer {S}cience, 4th International Symposium, {LFCS}'97,
{Y}aroslavl, {R}ussia, {J}uly 6--12, 1997, Proceedings},
year = {1997},
editor = {Sergei Adian and Anil Nerode},
volume = {1234},
series = {Lecture Notes in Computer Science},
pages = {266--275},
publisher = {Springer},
doi = {10.1007/3-540-63045-7_27},
abstract = {The operational logic of proofs~$\mathcal{LP}$ was introduced by S.~Artemov~\cite{Art95TR} as an operational version of~$S4$.
In this paper, we define a model for~$\mathcal{LP}$ and prove the corresponding completeness theorem.
Using this model, we prove the decidability of a variant of~$\mathcal{LP}$ axiomatized by a finite set of schemes.}
}
@techreport{Nog94TR,
author = {Elena Nogina},
title = {Logic of {P}roofs with the strong provability operator},
institution = {Institute for Logic, Language and Computation, University of Amsterdam},
year = {1994},
number = {ML--1994--10},
month = oct,
ps = {http://www.illc.uva.nl/Publications/ResearchReports/ML-1994-10.text.ps.gz},
abstract = {Logics with the strong provability operator ``...~\emph{is true and provable}'' together with the proof operators ``$p$~\emph{is a proof of}~...'' are axiomatized.
Kripkestyle completeness, decidability and arithmetical completeness of these logics are established.}
}
@article{Nog96FAM,
author = {E[lena] Nogina},
title = {Grzegorczyk logic with arithmetical proof operators},
journal = {Fundamental and Applied Mathematics},
year = {1996},
volume = {2},
number = {2},
pages = {483--499},
note = {In Russian},
http = {http://mech.math.msu.su/~fpm/eng/96/962/96206h.htm},
mathnet = {http://mi.mathnet.ru/eng/fpm162},
russian = {http://www.mathnet.ru/php/getFT.phtml?jrnid=fpm&paperid=162&volume=2&year=1996&issue=2&fpage=483&what=fullt&option_lang=eng},
keywords = {provability, modal logic, Kripke model, arithmetical completeness, decidability},
abstract = {Logics with the modal operator ``...~is true and provable'' together with the modal proof operator ``p~is a proof of~...'' are axiomatized.
Kripke-style completeness, decidability and arithmetical completeness of these logics are established.}
}
@inproceedings{Nog06LC,
author = {Elena Nogina},
title = {On logic of proofs and provability},
booktitle = {2005~Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'05,
{A}thens, {G}reece, {J}uly~28--{A}ugust~3, 2005},
year = {2006},
volume = {12(2)},
series = {Bulletin of Symbolic Logic},
pages = {356},
month = jun,
publisher = {Association for Symbolic Logic},
note = {Abstract presented by title},
ps = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps},
doi = {10.2178/bsl/1146620064},
abstract = {Joint logics of proofs and provability were studied in~\cite{Art94APAL} and~\cite{TYav01APAL}.
The latter found an arithmetically complete logic which contained both the provability logic~$\mathsf{GL}$~([Boo93])
and the logic of proofs~$\mathsf{LP}$~(\cite{Art01BSL}) in their joint language augmented by some additional operations.
A recent application in the logic of knowledge~\cite{ArtNog05TR} prompted a question of a complete axiomatization
of the logic of proofs and provability in the original language of~$\mathsf{GL}$ and~$\mathsf{LP}$.
In the current note we find such an axiomatization,~$\mathsf{GLA}$,
consisting of axioms and rules of~$\mathsf{GL}$ and~$\mathsf{LP}$ together with axioms $t:P \to []P$, $\neg t:P \to []\neg t:P$, $t:[]P \to P$,
and the reflection rule $\vdash []P~\Rightarrow~\vdash P$.
$\mathsf{GLA}$~has been supplied with a corresponding Kripke-style semantics and shown to be complete with respect to the intended arithmetical provability interpretation.}
}
@inproceedings{Nog07ASL,
author = {Elena Nogina},
title = {Epistemic completeness of {GLA}},
booktitle = {2007 Annual Meeting of the Association for Symbolic Logic,
{U}niversity of {F}lorida, {G}ainesville, {F}lorida, {M}arch 10--13, 2007},
year = {2007},
volume = {13(3)},
series = {Bulletin of Symbolic Logic},
pages = {407},
month = sep,
publisher = {Association for Symbolic Logic},
conference = {http://www.math.ufl.edu/~jal/logicyear/asl/},
doi = {10.2178/bsl/1186666153},
note = {Abstract},
ps = {http://www.math.ucla.edu/~asl/bsl/1303/1303-005.ps},
abstract = {The logic of proofs and provability~$\mathsf{GLA}$~\cite{Nog06LC} is an arithmetically complete system
that combines the provability logic~$\mathsf{GL}$ and Artemov's Logic of Proofs~$\mathsf{LP}$ (cf.~\cite{Art07MLH}) in their joint language.
$\mathsf{GLA}$~has become a prototype of epistemic logics with justification~\cite{Art07MLH}, \cite{ArtNog05TARK}, \cite{ArtNog05JLC}.
In addition to axioms and rules of~$\mathsf{LP}$ and~$\mathsf{GL}$, $\mathsf{GLA}$~has axioms $t:\varphi \to []\varphi$, $\neg t:\varphi \to []\neg t:\varphi$, $t:[]\varphi \to \varphi$,
and a rule $\vdash []\varphi~\Rightarrow~\vdash \varphi$.
In this paper we establish the completeness of~$\mathsf{GLA}$ with respect to epistemic semantics.
An epistemic model for~$\mathsf{GLA}$ is a Fitting~-- Artemov model (cf.~Def.~2 of~\cite{Art06TCS}) with\\
$-$ a reverse well-founded transitive frame~$(W,<)$\\
$-$ an equivalence relation~$\equiv$ on~$W$ as an evidence accessibility relation such that $< \subseteq \equiv$\\
$-$ a possible evidence function~(\cite{Art06TCS}, \cite{Fit05APAL})~$\mathcal{E}$ satisfying the stability property:
\[
\mathcal{E}(u, t) = \mathcal{E}(v, t) \textup{ whenever } u \equiv v.
\]}
}
@inproceedings{Nog09LC,
author = {Elena Nogina},
title = {Logic of strong provability and explicit proofs},
booktitle = {2008 {E}uropean Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'08,
{B}ern, {S}witzerland, {J}uly~3--{J}uly~8, 2008},
publisher = {Association for Symbolic Logic},
year = {2009},
volume = {15(1)},
series = {Bulletin of Symbolic Logic},
pages = {124--125},
month = mar,
note = {Abstract},
ps = {http://www.math.ucla.edu/~asl/bsl/1501/1501-005.ps},
doi = {10.2178/bsl/1231081772},
abstract = {Strong provability $F$~\emph{is true and provable in Peano Arithmetic} is known~([Boo93]) to be propositionally axiomatized by Grzegorczyk's logic~$\mathsf{Grz}$,
which postulates are classical logic axioms and rules, $[](F \to G) \to ([]F \to []G)$, $[]F \to [][]F$, $[]F \to F$, $[]([](F \to []F) \to F) \to F$,
and Rule of Necessitation: $\vdash F \Rightarrow \vdash []F$.
Artemov's Logic of Proofs~$\mathsf{LP}$~(\cite{Art01BSL}) axiomatizes proof operators \emph{$t$~is a proof of~$F$ in Peano Arithmetic}.
The postulates of~$\mathsf{LP}$ are the ones of the classical propositional logic, $t:(F \to G) \to (s:F \to (t\cdot s):G)$,
$t:F \to F$, $t:F \to !t:(t:F)$, $s:F \to (s+t):F$ and $t:F \to (s+t):F$,
and the rule of inferring~$c:A$ whenever $A$~is an axiom and $c$~is a proof constant.
Joint logics of proofs and provability have been studied in a variety of languages~(\cite{Art94APAL}, \cite{Nog94TR}, \cite{Nog06LC}, \cite{Nog07ASL}, \cite{TYav01APAL}).
In this paper we found the arithmetically complete logic of strong provability and explcit proofs~$\mathsf{GrzA}$ in the joint language of~$\mathsf{Grz}$ and~$\mathsf{LP}$.
$\mathsf{GrzA}$~consists of axioms and rules of~$\mathsf{Grz}$ and $\mathsf{LP}$ together with axioms $t:P \to []P$ and $\neg t:P \to []\neg t:P$.
We show that $\mathsf{GrzA}$~is complete with respect to the arithmetical provability interpretation,
supplied with a corresponding Fitting epistemic semantics and enjoys some sort of a finite model property,
which also yields the decidability of~$\mathsf{GrzA}$ for any given finite specification of constants.}
}
@inproceedings{Pac05PLS,
author = {Eric Pacuit},
title = {A Note on Some Explicit Modal Logics},
booktitle = {Proceedings of the 5th~{P}anhellenic {L}ogic {S}ymposium},
year = {2005},
month = jul # { 25--28,},
address = {Athens, Greece},
publisher = {University of {A}thens},
pages = {117--125},
conference = {http://cgi.di.uoa.gr/~pls5/},
pdf = {http://www.softlab.ntua.gr/~nickie/tmp/pls5/pacuit.pdf},
abstract = {Artemov introduced the Logic of Proofs~($\mathbf{LP}$) as a logic of explicit proofs.
We can also offer an epistemic reading of this formula: ``$t$~is a possible justification of~$\phi$''.
Motivated, in part, by this epistemic reading, Fitting introduced a Kripke style semantics for~$\mathbf{LP}$ in~\cite{Fit05APAL}.
In this note, we prove soundness and completeness of some axiom systems which are not covered in~\cite{Fit05APAL}.}
}
@techreport{Pac06TR,
author = {Eric Pacuit},
title = {A Note on Some Explicit Modal Logics},
institution = {Institute for Logic, Language and Computation, University of Amsterdam},
year = {2006},
number = {PP--2006--29},
pdf = {http://www.illc.uva.nl/Publications/ResearchReports/PP-2006-29.text.pdf},
note = {Published as~\cite{Pac05PLS}},
abstract = {Artemov introduced the Logic of Proofs~($\mathbf{LP}$) as a logic of explicit proofs.
We can also offer an epistemic reading of this formula: ``$t$~is a possible justification of~$\phi$''.
Motivated, in part, by this epistemic reading, Fitting introduced a Kripke style semantics for~$\mathbf{LP}$ in~\cite{Fit05APAL}.
In this note, we prove soundness and completeness of some axiom systems which are not covered in~\cite{Fit05APAL}.}
}
@inproceedings{Par05TARK,
author = {Rohit Parikh},
title = {Logical Omniscience and Common Knowledge; {WHAT} do we know and what do {WE} know?},
booktitle = {Theoretical {A}spects of {R}ationality and {K}nowledge, Proceedings of the Tenth Conference ({TARK~2005})},
year = {2005},
editor = {Ron van der Meyden},
pages = {62--77},
address = {Singapore},
publisher = {National University of Singapore},
month = jun # { 10--12,},
conference = {http://www.tark.org/tark05.htm},
pdf = {http://www.tark.org/proceedings/tark_jul10_05/p62-parikh.pdf},
abstract = {\emph{Two difficult issues for the logic of knowledge have been logical omniscience and common knowledge.
Our existing logics of knowledge based on Kripke structures seem to justify logical omniscience,
but we know that in real life it does not exist.
Also, common knowledge appears to be needed for certain real life procedures to work.
But it seems quite implausible that it actually exists in real people.
We suggest two} procedure based \emph{semantics for knowledge which seem to take care of both these issues in a relatively realistic way.
What this suggests is that if we really want to understand knowledge, then} existing customs \emph{and} plans \emph{must play a greater role than we are used to assigning them.}}
}
@incollection{Pog10LogKCA,
author = {Francesca Poggiolesi},
title = {Towards a Satisfying Proof Analysis of the Logic of Proofs},
booktitle = {{LogKCA-10}, Proceedings of the Second {ILCLI} International Workshop on Logic and Philosophy of Knowledge, Communication and Action},
publisher = {University of the Basque Country Press},
year = {2010},
editor = {Xabier Arrazola and Mar{\'{\i}}a Ponte},
pages = {371--385},
conference = {http://www.ilcli.ehu.es/p287-content/en/contenidos/informacion/ilcli_conferences/en_confe/conferences.html},
abstract = {The logic of proofs is an interesting and important logic recently introduced by Artemov~\cite{Art02CSLI}.
There exist two systems of the logic of proofs:
one that cas a classical base~$\mathbf{Lp}$,
and one that has an intuitionistic base~$\mathbf{Ilp}$.
From a Gentzen-style point of view, we can formulate two similar sequent calculi for the two systems~$\mathbf{Lp}$ and~$\mathbf{Ilp}$, respectively
(see~\cite{Art02CSLI}).
Although simple and cut-free, these two sequent calculi present several and analogous disadvantages:
they do not satisfy the subformula property,
their contraction rules are not admissible,
and their logical rules fail to be symmetric.
Therefore we can claim that at the proof theoretical level both the intuitionistic and the classical logic of proofs need to be improved.
In this paper we aim at dealing with this task.}
}
@mastersthesis{Pul10M,
author = {Cornelia Pulver},
title = {Self-Referentiality in Contraction-free Fragments of Modal Logic~{S4}},
school = {Institute of Computer Science and Applied Mathematics, University of Bern},
year = {2010},
pdf = {http://www.iam.unibe.ch/tilpub/2010/pul10.pdf}
}
@techreport{Ren04TR,
author = {Bryan Renne},
title = {Tableaux for the {L}ogic of {P}roofs},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2004},
number = {TR--2004001},
month = mar,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=94},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004001.pdf},
abstract = {The Logic of Proofs,~$\mathbf{LP}$, is an explicit provability logic due to Artemov.
The introduction of~$\mathbf{LP}$ answered a long-standing question concerning the intended semantics of G{\"{o}}del's provability calculus
and provability semantics for intuitionistic logic.
The explicit nature of~$\mathbf{LP}$ and its ability to naturally represent both modal logic and typed $\lambda$-calculi,
especially in light of the Curry-Howard Isomorphism,
makes its applicability to Computer Science a primary focus of research in this area.
In the present paper, I develop a tableau system for~$\mathbf{LP}$ and give a semantic proof of cut elimination.}
}
@techreport{Ren05TR,
author = {Bryan Renne},
title = {Propositional Games with Explicit Strategies},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2005},
number = {TR--2005012},
month = oct,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=165},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005012.pdf},
abstract = {This paper presents a game semantics for~$\mathsf{LP}$, Artemov's Logic of Proofs.
The language of~$\mathsf{LP}$ extends that of propositional logic by adding formula-labeling terms,
permitting us to take a term~$t$ and an $\mathsf{LP}$~formula~$A$ and form the new formula~$t:A$.
We define a game semantics for this logic that interprets terms as winning strategies on the formulas they label,
so $t:A$~may be read as ``$t$~is a winning strategy on~$A$.''
$\mathsf{LP}$~may thus be seen as a logic containing in-language descriptions of winning strategies on its own formulas.
We apply our semantics to show how winnable instances of certain extensive games with perfect information may be embedded into~$\mathsf{LP}$.
This allows us to use~$\mathsf{LP}$ to derive a winning strategy on the embedding,
from which we can extract a winning strategy on the original, non-embedded game.
As a concrete illustration of this method, we compute a winning strategy for a winnable instance of the well-known game~Nim.}
}
@incollection{Ren06ASLAPA,
author = {Bryan Renne},
title = {Games, strategies, and explicit knowledge},
booktitle = {2005--06~Winter Meeting of the {A}ssociation for {S}ymbolic {L}ogic,
The {H}ilton {N}ew {Y}ork {H}otel, {N}ew {Y}ork, {NY}, {D}ecember~27--29, 2005},
publisher = {Association for Symbolic Logic},
year = {2006},
volume = {12(3)},
series = {Bulletin of Symbolic Logic},
pages = {513},
month = sep,
note = {Abstract},
jstor = {http://www.jstor.org/stable/3699489},
ps = {http://www.math.ucla.edu/~asl/bsl/1203/1203-005.ps},
abstract = {Fitting has described~LP, Artemov's Logic of Proofs, as a logic of explicit knowledge.
To say that knowledge is explicit means that something is known for a specific reason,
as opposed to the Hintikka notion of knowledge, which is best described as knowability.
LP~introduces symbols for reasons along with natural operations to combine and manipulate them.
What results is a joint calculus of reasons and formulas, achieved by admitting new formulas of the form~$t:\varphi$,
which may be understood as ``$\varphi$~for reason~$t$.''
An evaluation game is a zero-sum game between two players with perfect information.
Given a model for a logical theory, the game is played on the parse tree of a formula,
but the rules of play are rigged so that the Verifier player has a winning strategy exactly when the formula holds in the model.
Interpreting a specific winning strategy for Verifier as a reason why Verifier can always win an evaluation game on an LP~formula in some LP~model,
we study the connection between reasons in logics of explicit knowledge and winning strategies in evaluation games.}
}
@incollection{Ren06WoLLIC,
author = {Bryan Renne},
title = {Propositional Games with Explicit Strategies},
booktitle = {Proceedings of the 13th {W}orkshop on {L}ogic, {L}anguage, {I}nformation and {C}omputation
({WoLLIC} 2006),
{S}tanford {U}niversity, {CA}, {USA}, 18--21 {J}uly 2006},
year = {2006},
editor = {G. Mints and R[uy] de Queiroz},
volume = {165},
series = {Electronic Notes in Theoretical Computer Science},
pages = {133--144},
month = nov,
publisher = {Elsevier},
note = {Journal version published as~\cite{Ren09IC}},
conference = {http://www.cin.ufpe.br/~wollic/wollic2006/},
doi = {10.1016/j.entcs.2006.05.042},
keywords = {Logic of Proofs, game-theoretic semantics, GTS},
abstract = {This paper introduces a game-theoretic semantics for~$\mathsf{LP}$, Artemov's Logic of Proofs,
taking the viewpoint that $\mathsf{LP}$~is a logic of explicit strategies on propositional verification games.
To demonstrate the utility of this viewpoint,
we define an embedding of the well-known game of~Nim into the propositional verification game,
which allows us to extract a winning strategy on a winnable Nim~instance by internalizing the proof in~$\mathsf{LP}$ of the formalized version of that instance.}
}
@inproceedings{Ren06ESSLLIStudent,
author = {Bryan Renne},
title = {Semantic Cut-elimination for Two Explicit Modal Logics},
booktitle = {Proceedings of the Eleventh {ESSLLI} Student Session,
18th~{E}uropean {S}ummer {S}chool in {L}ogic, {L}anguage and {I}nformation ({ESSLLI'}06)},
year = {2006},
address = {{M\'{a}}laga, {S}pain},
month = jul # {~31--} # aug # {~11,},
organization = {{FoLLI}},
editor = {Janneke Huitink and Sophia Katrenko},
pages = {148--158},
conference = {http://staff.science.uva.nl/~katrenko/stus06/},
pdf = {http://staff.science.uva.nl/~katrenko/stus06/images/renne.pdf},
proceedings = {http://folli.loria.fr/cds/2006/studentsession/Huitink.Katrenko.StudentSession.pdf},
abstract = {Explicit modal logics contain modal-like terms that label formulas in a way that mimics deduction in the system.
These logics have certain proof-theoretic advantages over the usual modal logics,
perhaps the most important of which is conventional cut-elimination.
The present paper studies tableau proof systems for two explicit modal logics, $\mathsf{LP}$ and~$\mathsf{S4LP}$.
Using a certain method to prove the correctness of these systems, we obtain a semantic proof of cut-elimination for these logics.}
}
@inproceedings{Ren06ESSLLIWRK,
author = {Bryan Renne},
title = {Bisimulation and Public Announcements in Logics of Evidence-Based Knowledge},
booktitle = {Proceedings of the
Workshop on {R}ationality and {K}nowledge,
18th~{E}uropean {S}ummer {S}chool in {L}ogic, {L}anguage and {I}nformation ({ESSLLI'}06)},
year = {2006},
address = {{M\'{a}}laga, {S}pain},
month = aug # { 7--11,},
editor = {Sergei [N.] Artemov and Rohit Parikh},
pages = {112--123},
organization = {{FoLLI}},
conference = {http://web.cs.gc.cuny.edu/~sartemov/rkw/},
pdf = {http://bryan.renne.org/docs/renne-bisimulation.pdf},
proceedings = {http://folli.loria.fr/cds/2006/workshops/Artemov.Parikh.RationalityAndKnowledge.pdf},
abstract = {This paper introduces a notion of bisimulation for Artemov's logics of evidence-based knowledge.
Bisimulation allows us to study the effect of dynamic epistemic operations on language expressivity.
It is shown that public announcements, a basic dynamic epistemic operation, add expressivity to the language of evidenced-based knowledge.
It is also shown that public announcements are definable in the language of evidence-based knowledge augmented with an evidence admissibility relation.}
}
@techreport{Ren07TR,
author = {Bryan Renne},
title = {Public Communication in Justification Logic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007025},
month = dec,
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=349},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007025.pdf},
abstract = {Justification Logic is the study of a family of logics used to reason about \emph{justified true belief}.
Dynamic Epistemic Logic is the study of a family of logics obtained by adding various kinds of communication to the language of multi-modal logic,
yielding languages for reasoning about communication and \emph{true belief}.
This paper is a first-step in merging these two areas,
in that it brings the most basic kind of communication studied in Dynamic Epistemic Logic---the public announcement---over to Justification Logic.
This gives us a language for reasoning about public announcements and justified true belief.
After giving an overview of Justification Logic, the paper introduces a notion of bisimulation for Justification Logic.
Bisimulation allows us to study the affect on language expressivity when we add various kinds of communication to the language.
Among a number of expressivity results, we show that adding public announcements to the language of Justification Logic strictly increases language expressivity.
This stands in contrast to the Plaza-Gerbrandy Theorem,
which states that adding public announcements to multi-modal logic does not increase language expressivity.
This leads us to extend the language of Justification Logic in order to provide a Plaza-Gerbrandy analog of multi-modal logic that we can use to reason about justified true belief.}
}
@phdthesis{Ren08PhD,
author = {Bryan Renne},
title = {Dynamic Epistemic Logic with Justification},
school = {CUNY Graduate Center},
year = {2008},
month = may,
pdf = {http://bryan.renne.org/docs/renne-dissertation.pdf},
abstract = {Justification Logic is the study of a family of logics used to reason about \emph{justified true belief}.
Dynamic Epistemic Logic is the study of logics used to reason about communication and \emph{true belief}.
This dissertation is a first step in merging these two areas,
in that it defines theories for a joint language in which we may reason about communication alongside justified true belief.
After some preliminary matters, we go through a comprehensive survey of Dynamic Epistemic Logic,
which primes us for the work at the end of the text.
We then move into the core work of the dissertation, where we introduce a number of extensions of existing languages and theories of Justification Logic.
Our extensions are all based on the work of Sergei Artemov,
who extended the language of propositional logic by the addition of formula-labeling terms.
This extension allows us to take a term~$t$ and a formula~$\varphi$ and form the new formula~$t:\varphi$.
The terms have a derivation-compatible structure that allows us to view terms as evidence verifying the truth of the formulas they label,
which provides us with a means for reasoning about \emph{justified true belief}.
We look at extensions of these theories that allow us to reason about evidence admissibility:
the new formula~$t>>\varphi$ lets us express that $t$~is admissible as evidence for~$\varphi$,
by which we mean that $t$~may be taken into account when considering the truth of~$\varphi$,
though $t$~need not conclusively validate~$\varphi$.
A further extension adds a unary modal operator~$[]$ that we use to reason about alternative evidence possibilities.
Nominaled extensions of the latter languages allow us to express a notion of dynamic evidence introduction,
whereby we may introduce a term~$t$ as admissible as evidence for~$\varphi$.
These extensions lead us to the final chapter of the text,
where we combine our various systems of Justification Logic with the framework of Dynamic Epistemic Logic.
Such joint theories contribute to the ongoing work aiming to provide a better foundational account of the reasoning of computational social agents.}
}
@inproceedings{Ren09TARK,
author = {Bryan Renne},
title = {Evidence Elimination in Multi-Agent Justification Logic},
booktitle = {Theoretical {A}spects of {R}ationality and {K}nowledge, Proceedings of the Twelfth Conference ({TARK~2009})},
year = {2009},
editor = {Aviad Heifetz},
pages = {227--236},
address = {Stanford University, California},
publisher = {ACM},
month = jul # { 6--8,},
doi = {10.1145/1562814.1562845},
pdf = {http://bryan.renne.org/docs/renne-elimination-tark09.pdf},
conference = {http://ai.stanford.edu/~epacuit/tark09/},
abstract = {This paper presents a logic combining \emph{Dynamic Epistemic Logic},
a framework for reasoning about multi-agent communication,
with a new multi-agent version of \emph{Justification Logic},
a framework for reasoning about evidence and justification.
This novel combination incorporates a new kind of \emph{multi-agent evidence elimination}
that cleanly meshes with the multi-agent communications from Dynamic Epistemic Logic,
resulting in a system for reasoning about multi-agent communication and evidence elimination for groups of interacting rational agents.}
}
@article{Ren09IC,
author = {Bryan Renne},
title = {Propositional games with explicit strategies},
journal = {Information and Computation},
year = {2009},
volume = {207},
number = {10},
pages = {1015--1043},
month = oct,
note = {Published online April~2009},
doi = {10.1016/j.ic.2008.11.005},
pdf = {http://bryan.renne.org/docs/renne-lpgames.pdf},
keywords = {Logic of Proofs, game semantics, Justification Logic},
abstract = {This paper presents a game semantics for~$\mathsf{LP}$, Artemov's Logic of Proofs.
The language of~$\mathsf{LP}$ extends that of propositional logic by adding formula-labeling terms,
permitting us to take a term~$t$ and an $\mathsf{LP}$~formula~$A$ and form the new formula~$t:A$.
We define a game semantics for this logic that interprets terms as winning strategies on the formulas they label,
so $t:A$~may be read as ``$t$~is a winning strategy on~$A$.''
$\mathsf{LP}$~may thus be seen as a logic containing in-language descriptions of winning strategies on its own formulas.
We apply our semantics to show how winnable instances of certain extensive games with perfect information may be embedded into~$\mathsf{LP}$.
This allows us to use~$\mathsf{LP}$ to derive a winning strategy on the embedding,
from which we can extract a winning strategy on the original, non-embedded game.
As a concrete illustration of this method, we compute a winning strategy for a winnable instance of the well-known game Nim.}
}
@article{Ren10JLC,
author = {Bryan Renne},
title = {Public communication in justification logic},
journal = {Journal of Logic and Computation},
year = {2010},
volume = {Advance Access},
number = {},
pages = {},
month = jul,
note = {},
doi = {10.1093/logcom/exq026},
keywords = {justification logic, bisimulation, public announcements, expressivity},
abstract = {Justification Logic is a framework for reasoning about evidence and justification in multi-agent systems.
Most accounts of Justification Logic are essentially static,
in that the (justified) beliefs of agents are immutable.
In this article,
we add public communication,
a dynamic operation of belief change studied in the area of Dynamic Epistemic Logic,
to the language of Justification Logic.
Introducing notions of bisimulation for the languages of Justification Logic with and without public communication,
we catalogue the expressive relationships that exist between almost all of the well-known static fragments of Justification Logic and
then determine whether the addition of public communication affects the various expressive relationships existing between these fragments.}
}
@incollection{Ren11SynLib,
author = {Bryan Renne},
title = {Simple Evidence Elimination in Justification Logic},
booktitle = {Dynamic Formal Epistemology},
publisher = {Springer},
year = {2011},
editor = {Patrick Girard and Olivier Roy and Mathieu Marion},
volume = {351},
series = {Synthese Library},
chapter = {7},
pages = {127--149},
doi = {10.1007/978-94-007-0074-1_7}
}
@mastersthesis{Rub03MT,
author = {Natalia M. Rubtsova},
title = {Logic of {P}roofs with Substitution},
school = {Lomonosov Moscow State University, Faculty of Mechanics and Mathematics},
year = {2003},
note = {In Russian}
}
@inproceedings{Rub06LC,
author = {N[atalia] M. Rubtsova},
title = {Evidence-based knowledge for {S5}},
booktitle = {2005~Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'05,
{A}thens, {G}reece, {J}uly~28--{A}ugust~3, 2005},
year = {2006},
volume = {12(2)},
series = {Bulletin of Symbolic Logic},
pages = {344--345},
month = jun,
publisher = {Association for Symbolic Logic},
conference = {http://www.math.uoa.gr/lc2005/},
note = {Abstract},
ps = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps},
doi = {10.2178/bsl/1146620064},
abstract = {Logics of evidence-based knowledge was proposed by S.~Artemov (see~\cite{Art04TR}).
It is multi-agent logic of knowledge enriched by evidence assertions of the form $t:\varphi$ where $t$~is an \emph{evidence term}.
Knowledge of every agent is axiomatized by a modal logic~$L$ ($L$~is~$T$ or~$S4$ or~$S5$),
evidence-based knowledge operator is described by the logic of proofs~$LP$ (see~\cite{Art01BSL}).
The resulting systems $L_nLP$ are provided with Kripke-style semantics.
The corresponding completeness theorems are proven.
For $L = T, S4$ it is shown that forgetful projection which replace all evidences by a uniform modality~$J$ coincides with~$L_nS4$.
We introduce the multi-agent logic of evidence-based knowledge $S4_nLP(S5)$ in which the evidence component corresponds to $S5$-modality.
In order to do this we extend the language of $S4_nLP$ by new unary operation of \emph{negative checker}~``$?$''.
Axioms and rules of $S4_nLP(S5)$ are those of $S4_nLP$ plus a new axiom describing negative checker:
\[
\neg[[t]]\varphi \to [[?t]]\neg[[t]]\varphi.
\]
For this logic we define Kripke-style models and prove the completeness theorem.
A \emph{model} is a structure $M = (W,R_1,...,R_n,R,\varepsilon,||-)$
where $W \ne \emptyset$ is a set of states, $R_i$, $R$~are reflexive transitive accessibility relations on~$W$.
An \emph{evidence} function~$\varepsilon$ is a mapping from states and evidence terms to sets of formulas.
It is monotonous ($uRv$~implies $\varepsilon(u, t) \subseteq \varepsilon(v, t)$) and
respects operations on evidence terms.
$||-$~is a validity relation between states and sentence variables.
The validity of formulas is defined in the usual way with the only new clause:
$u ||- [[t]]\varphi$ iff $\varphi \in \varepsilon(u, t)$.
We require that $\varphi \in \varepsilon(u, t)$ implies $v ||- \varphi$ for all $v \in W$ with~$uRv$.
\textbf{Theorem}. $S4_nLP(S5) \vdash \varphi$ iff $\varphi$~holds in all $S4_nLP(S5)$-models.}
}
@article{Rub06JLC,
author = {Natalia [M.] Rubtsova},
title = {On Realization of {$\mathsf{S5}$}-modality by Evidence Terms},
journal = {Journal of Logic and Computation},
year = {2006},
volume = {16},
number = {5},
pages = {671--684},
month = oct,
doi = {10.1093/logcom/exl030},
conference = {http://www.mccme.ru/ml2005/},
review = {http://www.ams.org/mathscinet/pdf/2269472.pdf},
abstract = {We introduce a logic of evidence-based knowledge~$\mathsf{S5}_n\mathsf{LP}(\mathsf{S5})$
in which the evidence part is based on logic of proofs with negative checker~$\mathsf{LP}(\mathsf{S5})$.
The later is obtained from the Logic of proofs~$\mathsf{LP}$
by adding a new unary operation of negative checker~`?' and the corresponding axiom.
We define Kripke-style models for~$\mathsf{S5}_n\mathsf{LP}(\mathsf{S5})$ and prove the completeness with respect to this semantics.
We also define the logic of justified knowledge for~$\mathsf{S5}_n\mathsf{LP}(\mathsf{S5})$.},
keywords = {Logic of proofs, logic of evidence-based knowledge, epistemic modal logic~$\mathsf{S5}$, logic of proofs with negative checker}
}
@incollection{Rub06CSR,
author = {Natalia [M.] Rubtsova},
title = {Evidence Reconstruction of Epistemic Modal Logic {$\mathsf{S5}$}},
booktitle = {Computer Science~--- Theory and Applications, First International {C}omputer {S}cience Symposium in {R}ussia, {CSR~2006},
{St.~P}etersburg, {R}ussia, {J}une 8--12, 2006, Proceedings},
year = {2006},
editor = {Dima Grigoriev and John Harrison and Edward A. Hirsch},
volume = {3967},
series = {Lecture Notes in Computer Science},
pages = {313--321},
publisher = {Springer},
doi = {10.1007/11753728_32},
conference = {http://logic.pdmi.ras.ru/~csr2006/},
abstract = {We introduce the logic of proofs whose modal counterpart is the modal logic~$\mathsf{S5}$.
The language of Logic of Proofs~$\mathsf{LP}$ is extended by a new unary operation of \emph{negative checker}~``?''.
We define Kripke-style models for the resulting logic in the style of Fitting models and prove the corresponding Completeness theorem.
The main result is the Realization theorem for the modal logic~$\mathsf{S5}$.}
}
@inproceedings{Rub06ESSLLI,
author = {Natalia [M.] Rubtsova},
title = {Semantics for Justification Logic Corresponding to {$\mathsf{S5}$}},
booktitle = {Proceedings of the
Workshop on {R}ationality and {K}nowledge,
18th~{E}uropean {S}ummer {S}chool in {L}ogic, {L}anguage and {I}nformation ({ESSLLI'}06)},
year = {2006},
address = {{M\'{a}}laga, {S}pain},
month = aug # { 7--11,},
organization = {{FoLLI}},
editor = {Sergei [N.] Artemov and Rohit Parikh},
pages = {124--132},
conference = {http://web.cs.gc.cuny.edu/~sartemov/rkw/},
pdf = {http://folli.loria.fr/cds/2006/workshops/Artemov.Parikh.RationalityAndKnowledge.pdf#page=131},
abstract = {We introduce a logic of evidence-based knowledge~$\mathsf{S5}_n\mathsf{LP}(\mathsf{S5})$
in which the evidence part is based on Logic of proofs with negative checker~$\mathsf{LP}(\mathsf{S5})$.
The later is obtained from the Logic of proofs~$\mathsf{LP}$ (S.~Artemov,~1995)
by adding a new unary operation of negative checker~``?'' and the corresponding axiom.
We define Fitting-Kripke-style models for~$\mathsf{S5}_n\mathsf{LP}(\mathsf{S5})$
and prove the completeness of~$\mathsf{S5}_n\mathsf{LP}(\mathsf{S5})$ with respect to this class of models
with various restrictions on accessibility relation for the evidence part.
We present the list of axioms for the logic~$\mathsf{S5}_n\mathsf{LP}(\mathsf{S5})^C$ with additional modality for common knowledge
and prove that this logic is the conservative extension of~$\mathsf{S5}_n\mathsf{LP}(\mathsf{S5})$.}
}
@article{Rub07MN,
author = {N[atalia] M. Rubtsova},
title = {Logic of {P}roofs with Substitution},
journal = {Mathematical Notes},
year = {2007},
volume = {82},
number = {5--6},
pages = {816--826},
month = nov,
doi = {10.1134/S0001434607110260},
review = {http://www.ams.org/mathscinet/pdf/2399970.pdf},
note = {Originally published in Russian},
abstract = {The substitution operation in logic of proofs is axiomatized.
For the system constructed, symbolic semantics is introduced and a completeness theorem is proved.},
keywords = {logic of proofs, axiomatics of substitution, symbolic semantic, symbolic model, finitely generated reflexive model, tableau of labels, semantic tableau, internalization}
}
@incollection{SedPod10LogKCA,
author = {Igor Sedl{\'{a}}r and Juraj Podrou{\v{z}}ek},
title = {Justification Logic as Dynamic Epistemic Logic?},
booktitle = {{LogKCA-10}, Proceedings of the Second {ILCLI} International Workshop on Logic and Philosophy of Knowledge, Communication and Action},
publisher = {University of the Basque Country Press},
year = {2010},
editor = {Xabier Arrazola and Mar{\'{\i}}a Ponte},
pages = {431--442},
conference = {http://www.ilcli.ehu.es/p287-content/en/contenidos/informacion/ilcli_conferences/en_confe/conferences.html},
abstract = {The paper presents a purely relational semantics for the basic justification logic~$\mathsf{J}$.
Soundness and completeness results are obtained be demonstrating a close connection of the purely relational semantics with Mkrtychev interpretations.
We prove that for every Mkrtychev interpretation there is an equivalent purely relational model and vice versa.
Then we sketch a dynamic epistemic interpretation of the purely relational semantics.
The paper concludes by pointing out the most interesting problems and topics for further study.}
}
@incollection{Sha10PCC,
author = {Daniyar S. Shamkanov},
title = {Strong normalization and confluence for reflexive combinatory logic},
booktitle = {{P}roof, {C}omputation, {C}omplexity {PCC~2010}, International Workshop, Proceedings},
publisher = {Institute of Computer Science and Applied Mathematics, University of Bern},
year = {2010},
editor = {Kai Br{\"u}nnler and Thomas Studer},
number = {IAM--10--001},
series = {{IAM~T}echnical Reports},
month = jun,
conference = {http://pcc2010.unibe.ch/},
http = {http://www.iam.unibe.ch/de/forschung/publikationen/techreports/2010/iam-10-001},
pdf = {http://www.iam.unibe.ch/de/forschung/publikationen/techreports/2010/iam-10-001/at_download/file},
note = {Abstract}
}
@incollection{Sha11WoLLIC,
author = {Daniyar S. Shamkanov},
title = {Strong Normalization and Confluence for Reflexive Combinatory Logic},
booktitle = {{L}ogic, {L}anguage, {I}nformation and {C}omputation, 18th~International {W}orkshop, {WoLLIC~2011},
{P}hiladelphia, {PA}, {USA}, {M}ay 18--20, 2011, Proceedings},
publisher = {Springer},
year = {2011},
editor = {Lev D. Beklemishev and Ruy de Queiroz},
volume = {6642},
series = {Lecture Notes in Artificial Intelligence},
pages = {228--238},
doi = {10.1007/978-3-642-20920-8_23},
conference = {http://wollic.org/wollic2011/},
abstract = {Reflexive combinatory logic~$\mathsf{RCL}$ was introduced by S.~Artemov as an extension of typed combinatory logic~$\mathsf{CL}_\rightarrow$
capable to internalize its own derivations of typing judgments.
It was designed as a basic theoretical prototype of functional programming languages extended by this kind of self-referential capacity.
However, its operational aspects remained to be clarified.
We study reductions for reflexive combinatory logic and prove strong normalization and confluence properties.}
}
@incollection{Sid94LFCS,
author = {Tatiana [L.] Sidon},
title = {Craig interpolation property in modal logics with provability interpretation},
booktitle = {Logical Foundations of Computer Science, Third International Symposium, {LFCS}'94,
{St.~P}etersburg, {R}ussia, {J}uly 11--14, 1994, Proceedings},
year = {1994},
editor = {A[nil] Nerode and Yu. V. Matiyasevich},
volume = {813},
series = {Lecture Notes in Computer Science},
pages = {329--340},
publisher = {Springer},
doi = {10.1007/3-540-58140-5_31}
}
@article{Sid97FAM,
author = {T[atiana] L. Sidon},
title = {Provability logic with operations over proofs},
journal = {Fundamental and Applied Mathematics},
year = {1997},
volume = {3},
number = {4},
pages = {1173--1197},
note = {In Russian},
http = {http://mech.math.msu.su/~fpm/eng/97/974/97418h.htm},
mathnet = {http://mi.mathnet.ru/eng/fpm269},
russian = {http://www.mathnet.ru/php/getFT.phtml?jrnid=fpm&paperid=269&volume=3&year=1997&issue=4&fpage=1173&what=fullt&option_lang=eng},
keywords = {propositional provability logics, operations over proofs, logics of proofs},
review = {http://www.ams.org/mathscinet/pdf/1794509.pdf},
abstract = {We present a natural axiomatization for propositional logic with modal operator for formal provability (Solovay,~[Sol76])
and labeled modalities for individual proofs with operations over them (Artemov,~\cite{Art95TR}).
For this purpose the language is extended by two new operations.
The obtained system~$\mathcal{MLP}$ naturally includes both Solovay's provability logic~GL and Artemov's operational modal logic~$\mathcal{LP}$.
All finite extensions of the basic system~$\mathcal{MLP}_0$ are proved to be decidable and arithmetically complete.
It is shown that $\mathcal{LP}$~realizes all operations over proofs admitting description in the modal propositional language.}
}
@incollection{Sid97LFCS,
author = {Tatiana [L.] Sidon},
title = {Provability logic with operations on proofs},
booktitle = {Logical {F}oundations of {C}omputer {S}cience, 4th International Symposium, {LFCS}'97,
{Y}aroslavl, {R}ussia, {J}uly 6--12, 1997, Proceedings},
year = {1997},
editor = {Sergei Adian and Anil Nerode},
volume = {1234},
series = {Lecture Notes in Computer Science},
pages = {342--353},
publisher = {Springer},
doi = {10.1007/3-540-63045-7_35},
abstract = {We present a natural axiomatization for propositional logic with a modal operator for formal provability~(Solovay,~[Sol76])
and labeled modalities for individual proofs with operations on them (Artemov,~\cite{Art95TR}).
For this purpose, the language has to be extended by two new operations.
The obtained system~$\mathcal{MLP}$ naturally includes both Solovay's provability logic~GL and Artemov's operational modal logic~$\mathcal{LP}$.
We prove that the system~$\mathcal{MLP}$ is decidable and arithmetically complete.
We also show that~$\mathcal{MLP}$ realizes all operations on proofs admitting description in the modal propositional language.}
}
@phdthesis{Sid97PhD,
author = {Tatiana L. Sidon},
title = {Dynamic logics of proofs with the provability operator},
school = {Lomonosov Moscow State University, Faculty of Mechanics and Mathematics},
year = {1997},
note = {In Russian}
}
@article{Sid98MUMBa,
author = {T[atiana] L. Sidon},
title = {Craig interpolation property for operational logics of proofs},
journal = {Moscow University Mathematics Bulletin},
year = {1998},
volume = {53},
number = {2},
pages = {37--41},
note = {Originally published in Russian},
bl = {http://direct.bl.uk/research/05/07/RN050535563.html},
review = {http://www.ams.org/mathscinet/pdf/1706144.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:01974820&type=pdf&format=complete}
}
@article{Sid98MUMBb,
author = {T[atiana] L. Sidon},
title = {Nonaxiomatizability of predicate logics of proofs},
journal = {Moscow University Mathematics Bulletin},
year = {1998},
volume = {53},
number = {6},
pages = {17--21},
note = {Originally published in Russian},
review = {http://www.ams.org/mathscinet/pdf/1710895.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:01974899&type=pdf&format=complete},
bl = {http://direct.bl.uk/research/05/07/RN060534597.html}
}
@techreport{Str93TR,
author = {Tyko Stra{\ss}en},
title = {Syntactical Models and Fixed Points for the Basic Logic of Proofs},
institution = {Institute of Computer Science and Applied Mathematics, University of Bern},
year = {1993},
number = {iam--93--020},
http = {http://www.iam.unibe.ch/publikationen/techreports/1993/iam-93-020},
psgza = {http://www.iam.unibe.ch/publikationen/techreports/1993/iam-93-020/file/at_download},
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 principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.}
}
@phdthesis{Str94PhD,
author = {Tyko Stra{\ss}en},
title = {The Basic Logic of Proofs},
school = {University of Bern},
year = {1994},
month = apr,
pdf = {http://www.strassen.us/thesis.pdf},
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.}
}
@article{Str94AMAI,
author = {Tyko Stra{\ss}en},
title = {Syntactical models and fixed points for the basic logic of proofs},
journal = {Annals of Mathematics and Artificial Intelligence},
year = {1994},
volume = {12},
number = {3--4},
pages = {291--321},
month = dec,
doi = {10.1007/BF01530789},
conference = {http://www.dagstuhl.de/9338},
abstract = {The Basic Logic of Proofs provides prepositional 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.}
}
@techreport{Wan09TR,
author = {Ren-June Wang},
title = {On Proof Realization on Modal Logic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2009},
number = {TR--2009003},
month = apr,
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2009003.pdf},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=374},
abstract = {Artemov's \emph{Logic of Proof},~$\mathsf{LP}$, is an explicit proof counterpart of~$\mathsf{S4}$.
Their formal connection is built through the \emph{realization theorem},
that every $\mathsf{S4}$~theorem can be converted to an $\mathsf{LP}$~theorem
by substituting \emph{proof terms} for provability modals.
Instead of the realization of theorems, what is concerned in this paper is the realization of proofs.
We will show that only a subclass of $\mathsf{S4}$~proofs, called non-circular proofs,
can be realized as $\mathsf{LP}$~proofs in this way.
Furthermore, we introduce a numerical version of~$\mathsf{LP}$, called~$\mathsf{S4}^\Delta$,
to constructively prove that every $\mathsf{S4}$~theorem has a non-circular proof.
These results provide a new algorithmic proof of the \emph{realization theorem}.}
}
@incollection{Wan09WoLLIC,
author = {Ren-June Wang},
title = {Knowledge, Time, and Logical Omniscience},
booktitle = {{L}ogic, {L}anguage, {I}nformation and {C}omputation, 16th {I}nternational {W}orkshop, {WoLLIC~2009},
{T}okyo, {J}apan, {J}une 21-24, 2009, Proceedings},
publisher = {Springer},
year = {2009},
editor = {Hiroakira Ono and Makoto Kanazawa and Ruy de Queiroz},
volume = {5514},
series = {Lecture Notes in Artificial Intelligence},
pages = {394--407},
doi = {10.1007/978-3-642-02261-6_31},
conference = {http://research.nii.ac.jp/wollic2009/},
abstract = {Knowledge's acquisition happens \emph{in} time.
However, this feature is not reflected in the standard epistemic logics,
e.g.~$\mathsf{S4}$~with its possible world semantics suggested by Hintikka in~[1],
and hence their applications are limited.
In this paper we adapt these normal modal logics to increase their expressive power
such that not only is \emph{what} is known modeled but also \emph{when} it is known is recorded.
We supplement each world with an awareness function which is an augmentation of
Fagin-Halpern's to keep track of the time when each formula is to be derived.
This provides a new response to the logical omniscience problem.
Our work originates from the tradition of study of \emph{Justification Logic},
also known as \emph{Logic of Proofs},~$\mathsf{LP}$, introduced by Artemov~([2],[3],[4]).
We will give the axiom systems of the models built here, accompanied with soundness and completeness results.}
}
@inproceedings{TYav00LC,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Provability logic with operations on proofs},
booktitle = {1999~{E}uropean Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'99,
{U}trecht, The {N}etherlands, {A}ugust 1--6, 1999},
year = {2000},
volume = {6(1)},
series = {Bulletin of Symbolic Logic},
pages = {132},
month = mar,
publisher = {Association for Symbolic Logic},
note = {Abstract},
conference = {http://old-www.cwi.nl/events/1999/lc99/?q=lc99/},
ps = {http://www.math.ucla.edu/~asl/bsl/0601/0601-007.ps},
euclid = {http://projecteuclid.org/euclid.bsl/1182353675},
jstor = {http://www.jstor.org/stable/421084},
abstract = {The idea of describing the intended Brouwer-Heyting-Kolmogorov semantics for intuitionistic logic by means of the modal logic of classical provability was suggested by G{\"{o}}del.
He introduced the modal logic of provability~$S4$ and defined intuitionistic logic inside~$S4$.
However, the problem of finding the provability interpretation for~$S4$ itself was left open.
In particular, the studies of the modal logic complete under the straightforward interpretation of the modality~$[]$
as the provability formula in arithmetic led to the logic~$GL$ (see~[Sol76]) incompatible with~$S4$.
The above problems were solved in~\cite{Art95TR},
where Artemov found the complete axiom system for the logic of proofs~$\mathcal{LP}$ in the format ``$t$~is a proof of~$F$''
and showed that $\mathcal{LP}$~was sufficient to emulate the whole~$S4$.
Proof terms in~$\mathcal{LP}$ are constructed by three elementary operations on proofs.
Our goal was to develop the joint logic that incorporates both the modality ``$F$~is provable'' and the proof operator ``$t$~is a proof of~$F$''.
We find the natural axiomatization~$\mathcal{MLP}$ of the minimal complete system that includes both~$GL$ and~$\mathcal{LP}$.
The presence of~$[]$ in the language of~$\mathcal{MLP}$ requires two new elementary operations on proofs.
We show that $\mathcal{MLP}$~suffices to realize all operations on proofs admitting description in the modal propositional language.
We also find the complete answer to the question of what versions of the interpolation property hold in~$\mathcal{LP}$.}
}
@inproceedings{TYav01LC,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Logic of proof and storage predicates},
booktitle = {2000~{E}uropean Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~2000,
{L}a {S}orbonne, {P}aris, {J}uly 23--31, 2000},
year = {2001},
volume = {7(1)},
series = {Bulletin of Symbolic Logic},
pages = {158--159},
month = mar,
publisher = {Association for Symbolic Logic},
note = {Abstract},
conference = {http://lc2000.logique.jussieu.fr/LC2000a.html},
ps = {http://www.math.ucla.edu/~asl/bsl/0701/0701-004.ps},
euclid = {http://projecteuclid.org/euclid.bsl/1182353767},
jstor = {http://www.jstor.org/stable/2687834},
abstract = {Propositional logic of proofs was introduced and studed by S.~Artemov in~\cite{Art95TR}.
He incorporated the proof predicate ``$t$~\emph{is a proof of}~$F$'' denoted by $t : F$
in the propositional language and found the complete axiom system for the logic of proofs~$\mathcal{LP}$.
Proofs are represented by proof terms constructed by three elementary operations on proofs
that realize application, (positive) proof checking and nondeterministic choice.
Artemov proved that $\mathcal{LP}$~is sufficient to realize the modality of the whole G{\"{o}}del's provability logic~$S4$ (see~[Goed33])
and thus provided~$S4$ with the intended provability reading.
We describe logic of proofs extended by the additional storage predicate~$[t]F$ with the informal reading ``$t$~\emph{knows about}~$F$''.
In the intended semantics $t$ is a reference for a text containing the information (knowledge)~$F$.
Some of the texts represent proofs.
This fact is denoted by~$t : F$.
Proofs contain only valid information that is reflected via the reflexivity principle $t : F \land [t]G \to G$.
The presence of the storage predicate allows us to specify operations on proofs depending on the formula arguments.
For example, negative proof checking that verifies whether $t$~is a proof of~$F$ and if no then returnes the proof of~$\neg(t : F)$
depends on both~$t$ and $F$. In our language we can replace~$F$ by the reference for $t : F$
\[
[a](t : F) \land \neg(t : F) \to \mathtt{check}(a) : (\neg t : F).
\]
We present the complete axiom system for the logic of proof and storage predicates $\mathcal{LPS}$.
The obtained system is sufficient to realize~$S4$ in such a way that the constructed realization makes sense for the arbitrary proof predicate.}
}
@article{TYav01APAL,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Logic of proofs and provability},
journal = {Annals of Pure and Applied Logic},
year = {2001},
volume = {113},
number = {1--3},
pages = {345--372},
month = dec,
doi = {10.1016/S0168-0072(01)00066-5},
review = {http://www.ams.org/mathscinet/pdf/1875751.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:01719236&type=pdf&format=complete},
keywords = {provability logic, logic of proofs, operations on proofs},
abstract = {In the paper the joint Logic of Proofs and Provability~$\mathcal{LPP}$ is presented that incorporates
both the modality~$[]$ for provability~([Sol76]) and the proof operator~$[[t]]F$ representing the proof predicate ``$t$~\emph{is a proof of}~$F$''~(\cite{Art95TR}).
The obtained system~$\mathcal{LPP}$ naturally includes both the modal logic of provability~GL and Artemov's Logic of Proofs~$\mathcal{LP}$.
The presence of the modality~$[]$ requires two new operations on proofs that together with operations of~$\mathcal{LP}$
allow to realize all the invariant operations on proofs admitting description in the modal propositional language.
Logic~$\mathcal{LPP}$ is proved to be decidable and complete with the intended provability semantics.}
}
@inproceedings{TYav03LC,
author = {Tatiana Yavorskaya},
title = {Axiomatic description of operations on proofs and labels},
booktitle = {2002 {E}uropean Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~'02,
{M\"{u}}nster, {G}ermany, {A}ugust 3--9, 2002},
year = {2003},
volume = {9(1)},
series = {Bulletin of Symbolic Logic},
pages = {118--119},
month = mar,
publisher = {Association for Symbolic Logic},
note = {Abstract presented by title},
ps = {http://www.math.ucla.edu/~asl/bsl/0901/0901-006.ps},
euclid = {http://projecteuclid.org/euclid.bsl/1046288727},
jstor = {http://www.jstor.org/stable/3087097},
abstract = {Logic of proofs~$\mathcal{LP}$ was introduced by S.~Artemov in~\cite{Art01BSL}.
It is formulated in the propositional language extended by atoms of the form~$[t]F$ which represent the proof predicate
``$t$~\emph{is a proof of a formula}~$F$''. Proofs are denoted by proof terms constructed by three elementary operations on proofs
(namely, application, (positive) proof checking and nondeterministic choice).
In~\cite{Art01BSL} $\mathcal{LP}$~is proved to be complete with respect to the intended semantics.
We extend the language of the logic of proofs by the additional labelling predicate~$x : F$
with the informal reading ``$x$~\emph{is a label for a formula}~$F$''.
A typical example of a labelling predicate is the relation ``$x$~\emph{is a code of a finite set of formulas containing}~$F$''.
Labelling predicate allows to specify operations on proofs depending on the formula argument.
For example, we can specify an operation for the proof of disjunction
\[
[t]A \land x : B \to [\mathsf{disj}(t,x)](A \lor B)
\]
and negative proof checker
\[
\neg[t]F \land x : F \to [\textup{$\mathsf{check}^{--}$}(t,x)](\neg[t]F).
\]
Different choices of operations on proofs and labels result in different logics.
We have proved that for a wide class of operations the corresponding logics are complete with respect to the intended arithmetical semantics.
Also, we study some natural examples of such logics.}
}
@article{TYav05JLC,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Negative Operations on Proofs and Labels},
journal = {Journal of Logic and Computation},
year = {2005},
volume = {15},
number = {4},
pages = {517--537},
month = aug,
doi = {10.1093/logcom/exi026},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:02215476&type=pdf&format=complete},
abstract = {Logic of proofs~$\mathcal{LP}$ introduced by S.~Artemov in~1995 describes properties of proof predicate `$t$~\emph{is a proof of}~$F$' in the propositional language
extended by atoms of the form $[[t]]F$.
Proof are represented by terms constructed by three elementary recursive operations on proofs.
In order to make the language more expressive we introduce the additional \emph{storage predicate} with the intended interpretation `$x$~\emph{is a label for}~$F$'.
It can play the role of syntax encoding, so it is useful for specification of operations that require formula arguments.
In this paper we study operations on proofs and labels that can be specified in the extended language.
First, we give a formal definition of an operation on proofs and labels.
Then, for an arbitrary finite set of operations~$\mathcal{F}$ the logic~$\mathcal{LPS}(\mathcal{F})$ is defined.
We provide~$\mathcal{LPS}(\mathcal{F})$ with symbolic semantics and arithmetical semantics.
The main result of the paper is the uniform completeness theorem for this family of logics with respect to the both types of semantics.}
}
@techreport{TYav05PR,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Negative operations on proofs and labels},
institution = {{L}ogic {G}roup {P}reprint {S}eries, {D}epartment of {P}hilosophy, {U}trecht {U}niversity},
year = {2005},
type = {Preprint},
number = {239},
month = jun,
note = {Later version published as \cite{TYav05JLC}},
pdf = {http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint239.pdf},
abstract = {Logic of proofs~$\mathcal{LP}$ introduced by S.~Artemov in~1995 describes properties of proof predicate ``$t$~\emph{is a proof of}~$F$''
in the propositional language extended by atoms of the form~$[[t]]F$.
Proof are represented by terms constructed by three elementary recursive operations on proofs.
In order to make the language more expressive we introduce the additional \emph{storage predicate} with the intended interpretation ``$x$~\emph{is a label for}~$F$''.
It can play the role of syntax encoding, so it is useful for specification of operations that require formula arguments.
In this paper we study operations on proofs and labels that can be specified in the extended language.
First, we give a formal definition of an operation on proofs and labels.
Then, for an arbitrary finite set of operations~$\mathcal{F}$ the logic~$\mathcal{LPS}(\mathcal{F})$ is defined.
We provide~$\mathcal{LPS}(\mathcal{F})$ with symbolic semantics and arithmetical semantics.
The main result of the paper is the uniform completeness theorem for this family of logics with respect to the both types of semantics.}
}
@article{TYav06JLC,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Logic of {P}roofs and Labels with a Complete Set of Operations},
journal = {Journal of Logic and Computation},
year = {2006},
volume = {16},
number = {5},
pages = {697--710},
month = oct,
doi = {10.1093/logcom/exl032},
conference = {http://www.mccme.ru/ml2005/},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:05142584&type=pdf&format=complete},
keywords = {logic of proofs, justification logic, modal logic, provability logic},
abstract = {We develop a framework in which operations on proofs can be specified and studied.
Proofs are treated as structures built from atomic proofs and references by means of computable operations.
Our approach extends the ideas of Logic of Proofs (Artemov,~1995,~\cite{Art01BSL})
in which the proof predicate `$t$~\emph{is a proof of}~$F$' is incorporated into the propositional language.
We introduce an additional storage predicate `$x$~\emph{is a label for}~$F$' (Yavorskaya,~2005,~\cite{TYav05JLC}).
In this article which is essentially a continuation of Yavorskaya’s work,
we study a natural example of a logic with operations on proofs and labels.
This logic~$\mathcal{LPS}^*$ is decidable and complete with respect to its intended semantics.
$\mathcal{LPS}^*$~is capable to internalize its own proofs,
and operations of~$\mathcal{LPS}^*$ suffice to realize all operations specified in the language with proofs and labels.}
}
@incollection{TYav06CSR,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Multi-agent Explicit Knowledge},
booktitle = {Computer Science~--- Theory and Applications, First International {C}omputer {S}cience Symposium in {R}ussia, {CSR~2006},
{St.~P}etersburg, {R}ussia, {J}une 8--12, 2006, Proceedings},
year = {2006},
editor = {Dima Grigoriev and John Harrison and Edward A. Hirsch},
volume = {3967},
series = {Lecture Notes in Computer Science},
pages = {369--380},
publisher = {Springer},
doi = {10.1007/11753728_38},
conference = {http://logic.pdmi.ras.ru/~csr2006/},
note = {Journal version published as~\cite{TYav08TOCS}},
abstract = {Logic of proofs~$\mathsf{LP}$, introduced by S.~Artemov,
originally designed for describing properties of formal proofs,
now became a basis for the theory of knowledge with justification.
So far, in epistemic systems with justification the corresponding ``evidence part'',
even for multi-agent systems, consisted of a single explicit evidence logic.
In this paper we introduce logics describing two interacting explicit evidence systems.
We find an appropriate formalization of the intended semantics
and prove the completeness of these logics with respect to both symbolic and arithmetical models.
Also, we find the forgetful projections for the logics with two proof predicates which are extensions of the bimodal logic $\mathsf{S4}^2$.}
}
@article{TYav08TOCS,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Interacting Explicit Evidence Systems},
journal = {Theory of Computing Systems},
year = {2008},
volume = {43},
number = {2},
pages = {272--293},
month = aug,
doi = {10.1007/s00224-007-9057-y},
note = {Published online October~2007},
keywords = {justification logic, explicit evidence, logic of proofs, multi-modal logic, epistemic logic},
abstract = {Logic of proofs~$\mathsf{LP}$, introduced by S.~Artemov,
originally designed for describing properties of formal proofs,
now became a basis for the theory of knowledge with justification (cf.~\cite{Art04TR}).
So far, in epistemic systems with justification the corresponding ``evidence part'',
even for multi-agent systems, consisted of a single explicit evidence logic.
In this paper we introduce logics describing two interacting explicit evidence systems.
We find an appropriate formalization of the intended semantics
and prove the completeness of these logics with respect to both symbolic and arithmetical models.
Also, we find the forgetful projections for the two-agent justification logics
which are extensions of the bimodal logic~$\mathsf{S4}^2$.}
}
@article{TYavRub07JANCL,
author = {T[atiana] {Yavorskaya (Sidon)} and N[atalia M.] Rubtsova},
title = {Operations on proofs and labels},
journal = {Journal of Applied Non-Classical Logics},
year = {2007},
volume = {17},
number = {3},
doi = {10.3166/jancl.17.283-316},
pages = {283--316},
keywords = {logic of proofs, justification logic, provability logic},
review = {http://www.ams.org/mathscinet/pdf/2364668.pdf},
abstract = {Logic of proofs~LP was introduced by S.~Artemov in~\cite{Art99JANCL}, \cite{Art01BSL}.
It describes properties of the proof predicate ``$t$~is a proof of~$F$'' formalized by the formula~$[[t]]F$.
Proofs are represented by terms constructed by three elementary recursive operations on proofs.
In this paper we extend the language of the logic of proofs by the additional storage predicate~$x F$ with the intended interpretation ``$x$~is a label for~$F$''.
The storage predicate can play the role of syntax encoding, so it is useful for specification of operations on proofs, especially those that require formula arguments.
We give a definition of a specification of an operation on proofs and introduce logics that describe such operations.
For a large class of operations we prove the completeness of these logics with respect to the intended semantics.
We also study the logic describing the operation of substitution.}
}
@incollection{RYav00CSL,
author = {Rostislav E. Yavorsky},
title = {On the Logic of the Standard Proof Predicate},
booktitle = {{C}omputer {S}cience {L}ogic, 14th~International Workshop,
{CSL}~2000, Annual Conference of the {EACSL},
{F}ischbachau, {G}ermany, {A}ugust~21--26, 2000, Proceedings},
year = {2000},
editor = {Peter G. Clote and Helmut Schwichtenberg},
volume = {1862},
series = {Lecture Notes in Computer Science},
pages = {527--541},
publisher = {Springer},
doi = {10.1007/3-540-44622-2_36},
conference = {http://www.tcs.informatik.uni-muenchen.de/csl2000/},
ps = {http://www.mi.ras.ru/~rey/papers/csl2000.ps},
keywords = {logic of proofs, semantics, protocolling extensions of theories},
abstract = {In~\cite{Art98TRb} S.~Artemov introduced the logic of proofs~$\mathcal{LP}$ describing provability in an arbitrary system.
In this paper we present the logic~$\mathcal{LPM}$ of the standard multiple conclusion proof predicate in Peano Arithmetic with the negative introspection operation.
We establish the completeness of~$\mathcal{LPM}$ with respect to the intended arithmetical semantics.
Two useful artificial semantics for~$\mathcal{LPM}$ were also found.
The first one is an extension of the usual boolean truth tables, whereas the second one deals with so-called protocolling extension of a theory.
For both cases the completeness theorem has been established.
In the last section we consider first order version of the logic~$\mathcal{LPM}$.
Arithmetical completeness of this logic is established too.}
}
@inproceedings{RYav01LC,
author = {Rostislav [E.] Yavorsky},
title = {Provability logics with quantifiers on proofs},
booktitle = {2000~{E}uropean Summer Meeting of the {A}ssociation for {S}ymbolic {L}ogic, {L}ogic {C}olloquium~2000,
{L}a {S}orbonne, {P}aris, {J}uly 23--31, 2000},
year = {2001},
volume = {7(1)},
series = {Bulletin of Symbolic Logic},
pages = {159},
month = mar,
publisher = {Association for Symbolic Logic},
note = {Abstract},
conference = {http://lc2000.logique.jussieu.fr/LC2000a.html},
ps = {http://www.math.ucla.edu/~asl/bsl/0701/0701-004.ps},
euclid = {http://projecteuclid.org/euclid.bsl/1182353767},
jstor = {http://www.jstor.org/stable/2687834},
abstract = {The language~$\mathit{qLP}$ of the provability logic with quantifiers on proofs contains
propositional letters, proof variables, boolean connectives, quantifiers over the proof variables and binary proof operator~$x : F$
(``$x$~is a proof of the formula~$F$'') introduced by S.~Artemov in~\cite{Art94APAL}.
This language naturally extends the language of the logic of proofs considered in~\cite{Art94APAL}.
The operational properties of provability studied in~\cite{Art98TRb} could be expressed in this language by the corresponding quantified sentences:
\[
\forall x \forall y \exists z (x : (A \to B) \to (y : A \to z : B)),
\]
\[
\forall x \exists y (x : A \to y : (x : A)), \textup{etc.}
\]
Also, this language may be considered as an extension of the propositional modal language,
since the modal provability operator~$[]A$ could be expressed by the formula~$\exists x (x : A)$.
An arithmetical interpretation~$*$ assigns arithmetical sentences to propositional variables,
commutes with boolean connectives and quantifiers and $(x : A)^* = \mathrm{Prf}(x, \lceil A^*\rceil)$.
(We suppose that the set of proof variables coincides with the set of individual variables in arithmetic.)
Given an arithmetical theory~$T$ and a class of proof predicates~$K$ we define the logic~$qLP_K(T)$
as the set of all formulas in the language~$qLP$, which are provable in~$T$ under every arithmetical interpretation~$*$ based on proof predicates from~$K$.
We present recent results concerning the decidability and arithmetical complexity of the corresponding logics for different~$T$ and~$K$.
It turned out that for many natural classes~$K$ the logic~$qLP_K(PA)$ is $\Pi_2^0$-hard.
For the case of the G{\"{o}}del proof predicate decidable fragments were found.}
}
@article{RYav01APAL,
author = {Rostislav E. Yavorsky},
title = {Provability logics with quantifiers on proofs},
journal = {Annals of Pure and Applied Logic},
year = {2001},
volume = {113},
number = {1--3},
pages = {373--387},
month = dec,
doi = {10.1016/S0168-0072(01)00067-7},
conference = {http://logic.pdmi.ras.ru/LogicDays},
ps = {http://www.mi.ras.ru/~rey/papers/apal.ps},
review = {http://www.ams.org/mathscinet/pdf/1875752.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:01719237&type=pdf&format=complete},
keywords = {provability logic, first-order logic of proofs},
abstract = {We study here extensions of the Artemov's logic of proofs in the language with quantifiers on proof variables.
Since the provability operator~$[]A$ could be expressed in this language by the formula~$\exists u[u]A$,
the corresponding logic naturally extends the well-known modal provability logic~$GL$.
Besides, the presence of quantifiers on proofs allows us to study some properties of provability not covered by the propositional logics.
In this paper we study the arithmetical complexity of the provability logic with quantifiers on proofs~$q\mathcal{LP}_{\mathcal{K}}(T)$
for a given arithmetical theory~$T$ and a class~$\mathcal{K}$ of proof predicates.
In the last section we define Kripke style semantics for the logics corresponding to the standard G{\"{o}}del proof predicate and its multiple conclusion version.}
}
@incollection{RYav02AiML,
author = {Rostislav E. Yavorsky},
title = {On Arithmetical Completeness of First-Order Logics of Provability},
booktitle = {Advances in Modal Logic, volume 3},
year = {2002},
editor = {Frank Wolter and Heinrich Wansing and Maarten de Rijke and Michael Zakharyaschev},
pages = {1--16},
publisher = {World Scientific},
conference = {http://www.aiml.net/conferences/aiml-2000/},
ps = {http://www.mi.ras.ru/~rey/papers/aiml2000.ps},
pubweb = {http://www.worldscibooks.com/compsci/5114.html},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:01989643&type=pdf&format=complete},
keywords = {provability logic, logic of proofs, first order extensions, arithmetical completeness, Kripke semantics},
abstract = {In this paper we consider first order extensions for the modal provability logic~$GL$ and the operational logic of proofs~$\mathcal{LP}$.
It is proved that if consider the case of so-called binding provability operator then a natural first order extension~$QGL^b$
of the logic~$GL$ turns out to be arithmetically complete.
The same holds for the first order logic of proofs~$\mathcal{QLP}^b$.
For the first order modal logic of provability~$QGL^b$ we also establish completeness with respect to Kripke style semantics.}
}
@unpublished{RYav03Unp,
author = {R[ostislav] E. Yavorsky},
title = {Undecidability of the minimal provability logic with quantifiers on proofs},
note = {Unpublished, in Russian},
year = {2003},
month = nov,
russian = {http://www.mi.ras.ru/~rey/papers/min_lpq.ps}
}
@article{RYav03PSIM,
author = {R[ostislav] E. Yavorskij},
title = {On Prenex Fragment of Provability Logic with Quantifiers on Proofs},
journal = {Proceedings of the Steklov Institute of Mathematics},
year = {2003},
volume = {242},
number = {3},
pages = {112--124},
mathnet = {http://mi.mathnet.ru/eng/tm410},
russian = {http://www.mi.ras.ru/~rey/papers/prenex.ps},
review = {http://www.ams.org/mathscinet/pdf/2054490.pdf},
abstract = {We consider a fragment of provability logic with quantifiers on proofs that consists of formulas with no occurrences of quantifiers in the scope of the proof predicate.
By definition, a logic~\textit{qL} is the set of formulas that are true in the standard model of arithmetic under every interpretation based on the standard G{\"{o}}del proof predicate.
We describe Kripke-style semantics for the logic~\textit{qL} and prove the corresponding completeness theorem.
For the case of injective arithmetical interpretations, the decidability is proved.}
}
@article{RYav05JLC,
author = {Rostislav [E.] Yavorskiy},
title = {On {K}ripke-style Semantics for the Provability Logic of {G\"{o}}del's Proof Predicate with Quantifiers on Proofs},
journal = {Journal of Logic and Computation},
year = {2005},
volume = {15},
number = {4},
pages = {539--549},
month = aug,
doi = {10.1093/logcom/exi037},
review = {http://www.ams.org/mathscinet/pdf/2157732.pdf},
keywords = {provability logic, logic of proofs, Kripke semantics, decidability},
abstract = {Kripke-style semantics is suggested for the provability logic with quantifiers on proofs corresponding to the standard G{\"{o}}del proof predicate.
It is proved that the set of valid formulas is decidable.
The arithmetical completeness is still an open issue.}
}
@techreport{RYav05PR,
author = {Rostislav [E.] Yavorskiy},
title = {On {K}ripke-style semantics for the provability logic of {G\"{o}}del's proof predicate with quantifiers on proofs},
institution = {{L}ogic {G}roup {P}reprint {S}eries, {D}epartment of {P}hilosophy, {U}trecht {U}niversity},
year = {2005},
type = {Preprint},
number = {238},
month = jun,
note = {Later version published as \cite{RYav05JLC}},
pdf = {http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint238.pdf},
abstract = {Kripke-style semantics is suggested for the provability logic with quantifiers on proofs corresponding to the standard G{\"{o}}del proof predicate.
It is proved that the set of valid formulas is decidable.
The arithmetical completeness is still an open issue.}
}
@techreport{Yu09TR,
author = {{YU}, Junhua},
title = {Prehistoric Phenomena and Self-referentiality in Realization Procedure},
institution = {Institute for Logic, Language and Computation, University of Amsterdam},
year = {2009},
number = {PP--2009--45},
month = nov,
note = {Later version published as~\cite{Yu10CSR}},
pdf = {http://www.illc.uva.nl/Publications/ResearchReports/PP-2009-45.text.pdf},
abstract = {By terms-allowed-in-types capacity,
the Logic of Proofs~\textbf{LP} includes formulas of the form~$t : \phi(t)$,
which have self-referential meanings.
In this paper,
``prehistoric phenomena'' in a Gentzen-style formulation of modal logic~\textbf{S4} are defined.
A special phenomenon,
i.e.,~``left prehistoric loop'',
is then shown to be necessary for self-referentiality in \textbf{S4-LP} realization.}
}
@incollection{Yu10CSR,
author = {Junhua Yu},
title = {Prehistoric Phenomena and Self-referentiality},
booktitle = {Computer Science --- Theory and Applications, 5th~International {C}omputer {S}cience Symposium in {R}ussia, {CSR~2010},
{K}azan, {R}ussia, {J}une 16--20, 2010, Proceedings},
publisher = {Springer},
year = {2010},
editor = {Farid Ablayev and Ernst W. Mayr},
volume = {6072},
series = {Lecture Notes in Computer Science},
pages = {384--396},
conference = {http://csr2010.antat.ru/},
doi = {10.1007/978-3-642-13182-0_38},
abstract = {By terms-allowed-in-types capacity, the Logic of Proofs~$\textbf{LP}$ enjoys a system of advanced combinatory terms,
while including types of the form~$t:\phi(t)$, which have self-referential meanings.
This paper suggests a research on possible $\textbf{S4}$~measures of self-referentiality introduced by this capacity.
Specifically, we define ``prehistoric phenomena'' in~$\textbf{G3s}$, a Gentzen-style formulation of modal logic~$\textbf{S4}$.
A special phenomenon, namely, ``left prehistoric loop'', is then shown to be necessary for self-referentiality in realizations of $\textbf{S4}$~theorems in~$\textbf{LP}$.}
}
@article{Zol97MUMB,
author = {E. E. Zolin},
title = {The {C}raig interpolation property in logics of proofs with a strong provability operator},
journal = {Moscow University Mathematics Bulletin},
year = {1997},
volume = {52},
number = {4},
pages = {39--41},
note = {Originally published in Russian},
review = {http://www.ams.org/mathscinet/pdf/1483062.pdf},
zmath = {http://www.zentralblatt-math.org/zmath/en/advanced/?q=an:01240161&type=pdf&format=complete}
}
This file was generated by bibtex2html 1.95.
Compiled by Roman Kuznets, 2011