@inproceedings{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},
springer = {http://dx.doi.org/10.1007/3-540-45504-3_2},
conference = {http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=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.}
}
@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 = {April},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2006004.pdf},
url = {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 = {June},
publisher = {Association for Symbolic Logic},
conference = {http://www.math.uoa.gr/lc2005/},
note = {Abstract},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps},
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 = {September},
publisher = {Association for Symbolic Logic},
note = {Abstract},
conference = {http://www.math.ufl.edu/~jal/logicyear/asl/},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1303/1303-005.ps},
abstract = {A multi-agent epistemic logic~$\mathbf{S4}_n^{CJ}$ is defined
which encompasses both traditional Common Knowledge~$C$ (cf.~[FagHalMosVar95, MeyvdHoe95])
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}).}
}
@inproceedings{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},
springer = {http://dx.doi.org/10.1007/978-3-540-72734-7_1},
conference = {http://lfcs.info/lfcs07/},
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.}
}
@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},
elsevier = {http://dx.doi.org/10.1016/0168-0072(94)90007-8},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/APAL94.ps},
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 = {December},
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 = {October},
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~([G{\"{o}}d33EMC]).
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}
}
@techreport{Art97TRc,
author = {Sergei N. Artemov},
title = {Proof Polynomials vs. {$\lambda$}-terms},
institution = {Cornell University},
year = {1997},
number = {CFIS 97--12},
month = {December}
}
@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 = {March},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CFIS98-06.ps}
}
@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 = {September},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CFIS98-10.ps}
}
@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 = {December},
note = {A later version is published as \cite{Art99CADE}}
}
@techreport{Art98TRd,
author = {Sergei N. Artemov},
title = {Explicit Modal Logic},
institution = {Cornell University},
year = {1998},
number = {CFIS 98--17},
month = {December},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/Upp.ps}
}
@inproceedings{Art00AiML,
author = {Sergei N. Artemov},
title = {Operations on Proofs that can be Specified by Means of Modal Logic},
booktitle = {Advances in Modal Logic, Second International Workshop,
{AiML}'98,
{U}niversity of {U}ppsala, {U}ppsala, {S}weden, {O}ctober 16--18, 1998},
year = {2000},
editor = {Michael Zakharyaschev and Krister Segerberg and Maarten de Rijke and Heinrich Wansing},
volume = {2},
series = {Advances in Modal Logic},
pages = {77--90},
publisher = {CSLI Publications},
conference = {http://www.aiml.net/conferences/aiml-1998/},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/AiML.ps}
}
@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 = {February},
note = {A later version is published as \cite{Art00AiML}}
}
@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 = {June},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CFIS99-07.ps}
}
@inproceedings{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},
elsevier = {http://dx.doi.org/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}
}
@inproceedings{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 Computer Science},
pages = {267--281},
publisher = {Springer},
springer = {http://dx.doi.org/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}
}
@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}
}
@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 = {March},
euclid = {http://projecteuclid.org/euclid.bsl/1182353754},
ps = {http://www.math.ucla.edu/~asl/bsl/0701/0701-001.ps}
}
@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},
pages = {89--119},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/CSLI.ps}
}
@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,
August 24--26, 2003, {S}teklov Institute of Mathematics, {St.~P}etersburg, {R}ussia},
year = {2003},
month = {August},
conference = {http://logic.pdmi.ras.ru/2ndDays/index.html},
abstract = {http://atlas-conferences.com/cgi-bin/abstract/cajy-40}
}
@inproceedings{Art03PSIM,
author = {S[ergei] N. Artemov},
title = {Embedding of the Modal {$\lambda$}-Calculus into the {L}ogic of {P}roofs},
booktitle = {Mathematical Logic and Algebra: Collected papers from the Conference
Dedicated to the 100th birthday of Academician {P}etr {S}ergeevich {N}ovikov, {M}oscow, {R}ussia, {A}ugust 2001},
year = {2003},
editor = {S[ergei] I. Adian},
volume = {242(3)},
series = {Proceedings of the Steklov Institute of Mathematics},
pages = {36--49},
publisher = {{MAIK} Nauka/Interperiodica},
mathnet = {http://mi.mathnet.ru/eng/tm404},
russian = {http://www.cs.gc.cuny.edu/~sartemov/publications/TSIM044.PS}
}
@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 = {November},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=140},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004018.pdf}
}
@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},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/RusMatSurveys.ps},
iop = {http://www.iop.org/EJ/abstract/0036-0279/59/2/R02}
}
@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}
}
@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 = {July},
elsevier = {http://dx.doi.org/10.1016/j.tcs.2006.03.009}
}
@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},
springer = {http://dx.doi.org/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 = {September},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=340},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007016.pdf}
}
@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 = {October},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=343},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007019.pdf}
}
@incollection{Art07MLH,
author = {Sergei [N.] Artemov},
title = {Modal logic in mathematics},
booktitle = {Handbook of Modal Logic},
publisher = {Elsevier},
year = {2007},
editor = {Patrick Blackburn and Johan van Benthem and Frank Wolter},
volume = {3},
series = {Studies in Logic and Practical Reasoning},
chapter = {16},
pages = {927--969},
elsevier = {http://dx.doi.org/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},
volume = {4800},
series = {Lecture Notes in Computer Science},
pages = {58--71},
month = {February},
springer = {http://dx.doi.org/10.1007/978-3-540-78127-1_4}
}
@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 = {November},
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},
springer = {http://dx.doi.org/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 {LFCS}~2007 submission},
year = {2006},
month = {December},
pdf = {http://www.lifia.info.unlp.edu.ar/~eduardo/lamIFull.pdf}
}
@inproceedings{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/},
springer = {http://dx.doi.org/10.1007/978-3-540-72734-7_2},
pdf = {http://www.lifia.info.unlp.edu.ar/~eduardo/publications/lfcs07.pdf}
}
@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},
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},
editor = {Aldo Ursini and Paolo Aglian{\`{o}}},
volume = {180},
series = {Lecture Notes in Pure and Applied Mathematics},
pages = {1--24}
}
@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},
pdf = {http://www.illc.uva.nl/D65/artemov.pdf},
conference = {http://www.illc.uva.nl/D65/}
}
@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 = {February},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005002.pdf},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=153}
}
@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 = {June},
euclid = {http://dx.doi.org/10.2178/jsl/1185803617},
ps = {http://www.phil.uu.nl/~iemhoff/logicproofs.ps}
}
@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 = {June},
publisher = {Association for Symbolic Logic},
note = {Abstract presented by title},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps}
}
@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},
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}
}
@inproceedings{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-Verlag},
springer = {http://dx.doi.org/10.1007/3-540-58140-5_4}
}
@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},
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}
}
@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 = {April},
elsevier = {http://dx.doi.org/10.1016/0168-0072(95)00062-3},
ps = {http://www.cs.gc.cuny.edu/~sartemov/publications/APAL96.ps}
}
@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}
}
@inproceedings{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/},
springer = {http://dx.doi.org/10.1007/11874683_9},
pdf = {http://kuznets.googlepages.com/csl06_with_Artemov.pdf}
}
@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 = {August},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004011.pdf},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=106}
}
@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 = {February},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005004.pdf},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=151}
}
@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,
{J}une 10--12, 2005, {N}ational {U}niversity of {S}ingapore, {S}ingapore},
year = {2005},
editor = {Ron van der Meyden},
pages = {279--294},
publisher = {National University of Singapore},
conference = {http://www.tark.org/tark05.htm},
pdf = {http://www.tark.org/proceedings/tark_jul10_05/p279-artemov.pdf}
}
@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 = {December},
oxford = {http://dx.doi.org/10.1093/logcom/exi053}
}
@inproceedings{ArtNog08CSR,
author = {Sergei [N.] Artemov and Elena Nogina},
title = {Topological Semantics of Justification Logic},
booktitle = {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},
springer = {http://dx.doi.org/10.1007/978-3-540-79709-8_7},
conference = {http://csr2008.ru/}
}
@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}
}
@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}
}
@inproceedings{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-Verlag},
springer = {http://dx.doi.org/10.1007/3-540-56992-8_3}
}
@inproceedings{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-Verlag},
springer = {http://dx.doi.org/10.1007/BFb0022556}
}
@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 = {October-December},
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}
}
@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},
pdf = {http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint235.pdf}
}
@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},
springer = {http://dx.doi.org/10.1007/0-387-31072-X_2}
}
@incollection{vanBen06PS,
author = {Benthem, Johan van},
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 = {March},
springer = {http://dx.doi.org/10.1007/s11098-005-4052-0},
pdf = {http://www.illc.uva.nl/Publications/ResearchReports/PP-2005-20.text.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}
}
@inproceedings{Bre01ESSLLI,
author = {Vladimir [N.] Brezhnev},
title = {On the Logic of Proofs},
booktitle = {Proceedings of the sixth {ESSLLI} Student Session, {A}ugust 2001, {H}elsinki},
year = {2001},
editor = {Kristina Striegnitz},
pages = {35--46},
proceedings = {http://folli.loria.fr/cds/2001/courses/readers/studentsession.pdf},
conference = {http://www.coli.uni-saarland.de/~kris/esslli01/}
}
@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 = {February},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=152},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005003.pdf}
}
@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 = {July},
elsevier = {http://dx.doi.org/10.1016/j.tcs.2006.03.010},
pdf = {http://kuznets.googlepages.com/BrezhnevKuznets06TCS.pdf}
}
@inproceedings{Bry05M4M,
author = {Yegor Bryukhov},
title = {Automatic proof search in logic of justified common knowledge},
booktitle = {Methods for Modalities, 4th International Workshop,
{M4M}'05,
{B}erlin, {G}ermany, {D}ecember 1--2, 2005, Proceedings},
year = {2005},
publisher = {{H}umboldt University},
conference = {http://m4m.loria.fr/M4M4/workshop.html},
pdf = {http://web.cs.gc.cuny.edu/~yegor/publications/m4m2005.pdf}
}
@phdthesis{Bry06PhD,
author = {Yegor Bryukhov},
title = {Integration of Decision Procedures into High-Order Interactive Provers},
school = {CUNY Graduate Center},
year = {2006},
pdf = {http://web.cs.gc.cuny.edu/~yegor/publications/YegorBryukhovThesis2006.pdf}
}
@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 = {September},
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 = {September},
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 = {October},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=118},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004016.pdf}
}
@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 = {December},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=146},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004019.pdf}
}
@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 = {February},
elsevier = {http://dx.doi.org/10.1016/j.apal.2004.04.009},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/LPSemantics.pdf}
}
@inproceedings{Fit05LY,
author = {Melvin Fitting},
title = {A Logic of Explicit Knowledge},
booktitle = {{L}ogica 2004,
18th International Symposium,
{H}ejnice Monastery, Czech Republic, {J}une 21--25, 2004, Selected papers},
publisher = {Filosofia},
year = {2005},
editor = {Libor B{\v{e}}hounek and Marta B{\'i}lkov{\'a}},
series = {Logica Yearbook 2004},
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}
}
@inproceedings{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. de Queiroz and A. Macintyre and G. Bittencourt},
volume = {143},
series = {Electronic Notes in Theoretical Computer Science},
pages = {59--71},
month = {January},
publisher = {Elsevier},
conference = {http://www.cin.ufpe.br/~wollic/wollic2005/},
elsevier = {http://dx.doi.org/10.1016/j.entcs.2005.04.038}
}
@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 = {March},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=174},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2006002.pdf}
}
@unpublished{Fit06Unp,
author = {Melvin Fitting},
title = {Realizations and {LP}},
note = {Unpublished},
year = {2006},
month = {August},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/RealizeTheorem.pdf}
}
@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 = {March},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=326},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007006.pdf}
}
@inproceedings{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},
springer = {http://dx.doi.org/10.1007/978-3-540-72734-7_15},
conference = {http://lfcs.info/lfcs07/}
}
@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 = {July},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=339},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007015.pdf}
}
@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 = {November},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007020.pdf},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=344}
}
@inproceedings{Fit08ISAIM,
author = {Melving Fitting},
title = {Explicit Logics of Knowledge and Conservativity},
booktitle = {Tenth International Symposium on Artificial Intelligence and Mathematics,
{ISAIM} 2008,
{F}ort {L}auderdale, {F}lorida, {J}anuary 2--4, 2008, Online Proceedings},
year = {2008},
conference = {http://isaim2008.unl.edu/},
pdf = {http://isaim2008.unl.edu/PAPERS/SS1-AI+Logic/MFitting-ss1.pdf}
}
@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 = {March},
elsevier = {http://dx.doi.org/10.1016/j.apal.2007.11.003},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/QLP.pdf}
}
@inproceedings{Fit08CSR,
author = {Melvin Fitting},
title = {{S4LP} and Local Realizability},
booktitle = {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},
springer = {http://dx.doi.org/10.1007/978-3-540-79709-8_19},
conference = {http://csr2008.ru/}
}
@incollection{Fit08Unp,
author = {Melvin Fitting},
title = {Reasoning With Justifications},
booktitle = {Towards Mathematical Philosophy},
publisher = {Springer},
year = {forthcoming},
editor = {David Makinson and Jacek Malinowski},
series = {Trends in Logic},
pdf = {http://comet.lehman.cuny.edu/fitting/bookspapers/pdf/papers/ReasoningJustifications.pdf}
}
@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},
year = {2005},
volume = {46},
series = {Oxford Logic Guides}
}
@techreport{Gor05TR,
author = {Evan Goris},
title = {Logic of Proofs for bounded arithmetic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2005},
number = {TR--2005011},
month = {October},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=164},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005011.pdf}
}
@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 = {March},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=173},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2006003.pdf}
}
@inproceedings{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},
springer = {http://dx.doi.org/10.1007/11753728_21},
conference = {http://logic.pdmi.ras.ru/~csr2006/}
}
@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 = {March},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=325},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007005.pdf}
}
@inproceedings{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},
springer = {http://dx.doi.org/10.1007/978-3-540-72734-7_17},
conference = {http://lfcs.info/lfcs07/}
}
@article{Gor08TCS,
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 = {August},
springer = {http://dx.doi.org/10.1007/s00224-007-9058-x},
note = {Published online in October 2007}
}
@inproceedings{HalPuc07TARK,
author = {Joseph Y. Halpern and Riccardo Pucella},
title = {Dealing With Logical Omniscience},
booktitle = {Proceedings of the 11th conference on
Theoretical {A}spects of {R}ationality and {K}nowledge 2007,
{B}russels, {B}elgium, {J}une 25--27, 2007},
year = {2007},
pages = {169--176},
publisher = {ACM},
acm = {http://doi.acm.org/10.1145/1324249.1324273},
conference = {http://www.info.fundp.ac.be/~pys/TARK07/},
pdf = {http://www.cs.cornell.edu/home/halpern/papers/pragmatics.pdf}
}
@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 = {March},
publisher = {Association for Symbolic Logic},
conference = {http://www.stanford.edu/~sommer/ASL.html},
note = {Abstract},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1201/1201-006.ps}
}
@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},
elsevier = {http://dx.doi.org/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},
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},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=81},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2003007.pdf}
}
@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 = {October},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=166},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005013.pdf}
}
@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 = {April},
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}
}
@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}
}
@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 = {July},
elsevier = {http://dx.doi.org/10.1016/j.tcs.2006.03.015}
}
@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 = {August},
elsevier = {http://dx.doi.org/10.1016/j.apal.2005.11.004}
}
@inproceedings{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 [I.] Adian and Anil Nerode},
volume = {1234},
series = {Lecture Notes in Computer Science},
pages = {167--177},
publisher = {Springer},
springer = {http://dx.doi.org/10.1007/3-540-63045-7_18},
ps = {http://lpcs.math.msu.su/~krupski/FLP_LNCS.PS}
}
@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}
}
@inproceedings{VKru02APAL,
author = {Vladimir N. Krupski},
title = {The single-conclusion proof logic and inference rules specification},
booktitle = {First {St.~P}etersburg Conference on Days of Logic and Computability,
{M}ay 26--29, 1999, {S}teklov Institute of Mathematics, {St.~P}etersburg, {R}ussia},
year = {2001},
editor = {Yuri [V.] Matiyasevich},
volume = {113(1--3)},
series = {Annals of Pure and Applied Logic},
pages = {181--206},
month = {December},
publisher = {Elsevier},
elsevier = {http://dx.doi.org/10.1016/S0168-0072(01)00058-6},
conference = {http://logic.pdmi.ras.ru/LogicDays},
ps = {http://lpcs.math.msu.su/~krupski/flpapal.ps}
}
@inproceedings{VKru06JLC,
author = {Vladimir N. Krupski},
title = {Reference Constructions in the Single-conclusion Proof Logic},
booktitle = {Computer Science Applications of Modal Logic, International Conference,
{M}oscow, {R}ussia, {S}eptember 5--9, 2005, Proceedings},
year = {2006},
editor = {Valentin Shehtman},
volume = {16(5)},
series = {Journal of Logic and Computation},
pages = {645--661},
publisher = {Oxford University Press},
month = {October},
oxford = {http://dx.doi.org/10.1093/logcom/exl028},
conference = {http://www.mccme.ru/ml2005/}
}
@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 = {July},
elsevier = {http://dx.doi.org/10.1016/j.tcs.2006.03.016},
pdf = {http://lpcs.math.msu.su/~krupski/lp_refel2.pdf}
}
@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 = {September},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=341},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007017.pdf}
}
@inproceedings{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},
springer = {http://dx.doi.org/10.1007/3-540-44622-2_25},
conference = {http://www.tcs.informatik.uni-muenchen.de/csl2000/},
pdf = {http://kuznets.googlepages.com/csl2000.pdf}
}
@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 = {March},
publisher = {Association for Symbolic Logic},
conference = {http://www.aladdin.cs.cmu.edu/asl/},
note = {Abstract},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1101/1101-005.ps}
}
@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 = {June},
note = {Abstract presented by title},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps}
}
@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 = {September},
note = {Abstract},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1203/1203-005.ps}
}
@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,
7--11~{A}ugust 2006, {U}niversidad de {M\'{a}}laga},
year = {2006},
editor = {Sergei [N.] Artemov and Rohit Parikh},
pages = {66--75},
month = {August},
conference = {http://web.cs.gc.cuny.edu/~sartemov/rkw/},
pdf = {http://kuznets.googlepages.com/esslli06.pdf},
proceedings = {http://folli.loria.fr/cds/2006/workshops/Artemov.Parikh.RationalityAndKnowledge.pdf}
}
@inproceedings{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/},
springer = {http://dx.doi.org/10.1007/978-3-540-72734-7_24},
pdf = {http://kuznets.googlepages.com/LFCS07.pdf}
}
@phdthesis{Kuz08PhD,
author = {Roman Kuznets},
title = {Complexity Issues in Justification Logic},
school = {CUNY Graduate Center},
year = {2008},
month = {May},
pdf = {http://kuznets.googlepages.com/PhD.pdf}
}
@inproceedings{Kuz08CSR,
author = {Roman Kuznets},
title = {Self-referentiality of Justified Knowledge},
booktitle = {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/},
springer = {http://dx.doi.org/10.1007/978-3-540-79709-8_24}
}
@inproceedings{Kuz08LC,
author = {Roman Kuznets},
title = {Complexity through tableaux in justification logic},
booktitle = {Logic Colloquium~2008, Bern, Switzerland, July 3--8, Abstracts of Plenary Talks, Tutorials,
Special Sessions, Contributed Talks},
year = {2008},
pages = {38--39},
conference = {http://www.lc08.iam.unibe.ch/},
note = {Abstract},
proceedings = {http://www.lc08.iam.unibe.ch/AbstractsBooklet.pdf}
}
@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 = {July},
springer = {http://dx.doi.org/10.1023/A:1005298816666}
}
@article{Mil07APAL,
author = {Robert 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 = {March},
elsevier = {http://dx.doi.org/10.1016/j.apal.2006.03.001}
}
@inproceedings{Mkr97LFCS,
author = {Alexey Mkrtychev},
title = {Models for the {L}ogic of {P}roofs},
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 [I.] Adian and Anil Nerode},
volume = {1234},
series = {Lecture Notes in Computer Science},
pages = {266--275},
publisher = {Springer},
springer = {http://dx.doi.org/10.1007/3-540-63045-7_27}
}
@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 = {October},
ps = {http://www.illc.uva.nl/Publications/ResearchReports/ML-1994-10.text.ps.gz}
}
@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},
emis = {http://www.emis.de/journals/FPM/eng/96/962/96206h.htm},
russian = {http://www.emis.de/journals/FPM/ps/96/962/96206.zip}
}
@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 = {June},
publisher = {Association for Symbolic Logic},
note = {Abstract presented by title},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps}
}
@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 = {September},
publisher = {Association for Symbolic Logic},
conference = {http://www.math.ufl.edu/~jal/logicyear/asl/},
note = {Abstract},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1303/1303-005.ps}
}
@inproceedings{Nog08LC,
author = {Elena Nogina},
title = {Logic of strong provability and explicit proofs},
booktitle = {Logic Colloquium~2008, Bern, Switzerland, July 3--8, Abstracts of Plenary Talks, Tutorials,
Special Sessions, Contributed Talks},
year = {2008},
pages = {43--44},
conference = {http://www.lc08.iam.unibe.ch/},
proceedings = {http://www.lc08.iam.unibe.ch/AbstractsBooklet.pdf},
note = {Abstract}
}
@inproceedings{Pac05PanHLS,
author = {Eric Pacuit},
title = {A Note on Some Explicit Modal Logics},
booktitle = {Proceedings of the 5th Panhellenic Logic Symposium,
{A}thens, {G}reece, {J}uly 25--28, 2005},
year = {2005},
publisher = {University of {A}thens},
conference = {http://cgi.di.uoa.gr/~pls5/},
pdf = {http://www.illc.uva.nl/Publications/ResearchReports/PP-2006-29.text.pdf}
}
@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}
}
@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,
{J}une 10--12, 2005, {N}ational {U}niversity of {S}ingapore, {S}ingapore},
year = {2005},
editor = {Ron van der Meyden},
pages = {62--77},
publisher = {National University of Singapore},
conference = {http://www.tark.org/tark05.htm},
pdf = {http://www.tark.org/proceedings/tark_jul10_05/p62-parikh.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 = {March},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=94},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2004001.pdf}
}
@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 = {October},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=165},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2005012.pdf}
}
@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 = {September},
note = {Abstract},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1203/1203-005.ps}
}
@inproceedings{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. de Queiroz},
volume = {165},
series = {Electronic Notes in Theoretical Computer Science},
pages = {133--144},
month = {November},
publisher = {Elsevier},
conference = {http://www.cin.ufpe.br/~wollic/wollic2006/},
elsevier = {http://dx.doi.org/10.1016/j.entcs.2006.05.042}
}
@inproceedings{Ren06ESSLLIStudent,
author = {Bryan Renne},
title = {Semantic Cut-elimination for Two Explicit Modal Logics},
booktitle = {Proceedings of the
Eleventh {ESSLLI} Student Session,
{J}une 20, 2006, {M\'{a}}laga, Spain},
year = {2006},
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}
}
@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,
7--11~{A}ugust 2006, {U}niversidad de {M\'{a}}laga},
year = {2006},
editor = {Sergei [N.] Artemov and Rohit Parikh},
pages = {112--123},
month = {August},
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}
}
@techreport{Ren07TRa,
author = {Bryan Renne},
title = {The Relative Expressivity of Public and Private Communication in {BMS} Logic},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2007},
number = {TR--2007012},
month = {May},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007012.pdf},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=336}
}
@inproceedings{Ren07WLRI,
author = {Bryan Renne},
title = {The Relative Expressivity of Public and Private Communication in {BMS} Logic},
booktitle = {A Meeting of the Minds: Proceedings of the
Workshop on Logic, Rationality and Interaction,
{B}eijing, 2007},
year = {2007},
editor = {Johan van Benthem and Shier Ju and Frank Veltman},
volume = {8},
series = {Texts in Computing},
pages = {213--229},
publisher = {College Publications},
conference = {http://www.illc.uva.nl/LORI/},
pdf = {http://bryan.renne.org/docs/renne-bmsPublicPrivate-vLORI.pdf}
}
@techreport{Ren07TRb,
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 = {December},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=349},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2007025.pdf}
}
@techreport{Ren08TR,
author = {Bryan Renne},
title = {Public and Private Communication are Different: Results on Relative Expressivity},
institution = {{CUNY} {P}h.{D}. {P}rogram in {C}omputer {S}cience},
year = {2008},
number = {TR--2008001},
month = {February},
http = {http://www.cs.gc.cuny.edu/tr/techreport.php?id=350},
pdf = {http://www.cs.gc.cuny.edu/tr/files/TR-2008001.pdf}
}
@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}
}
@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 = {June},
publisher = {Association for Symbolic Logic},
conference = {http://www.math.uoa.gr/lc2005/},
note = {Abstract},
proceedings = {http://www.math.ucla.edu/~asl/bsl/1202/1202-007.ps}
}
@inproceedings{Rub06JLC,
author = {Natalia [M.] Rubtsova},
title = {On Realization of {$\mathsf{S5}$}-modality by Evidence Terms},
booktitle = {Computer Science Applications of Modal Logic, International Conference,
{M}oscow, {R}ussia, {S}eptember 5--9, 2005, Proceedings},
year = {2006},
editor = {Valentin Shehtman},
volume = {16(5)},
series = {Journal of Logic and Computation},
pages = {671--684},
publisher = {Oxford University Press},
month = {October},
oxford = {http://dx.doi.org/10.1093/logcom/exl030},
conference = {http://www.mccme.ru/ml2005/}
}
@inproceedings{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},
springer = {http://dx.doi.org/10.1007/11753728_32},
conference = {http://logic.pdmi.ras.ru/~csr2006/}
}
@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,
7--11~{A}ugust 2006, {U}niversidad de {M\'{a}}laga},
year = {2006},
editor = {Sergei [N.] Artemov and Rohit Parikh},
pages = {124--132},
conference = {http://web.cs.gc.cuny.edu/~sartemov/rkw/},
proceedings = {http://folli.loria.fr/cds/2006/workshops/Artemov.Parikh.RationalityAndKnowledge.pdf}
}
@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 = {November},
springer = {http://dx.doi.org/10.1134/S0001434607110260}
}
@inproceedings{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 [I.] Adian and Anil Nerode},
volume = {1234},
series = {Lecture Notes in Computer Science},
pages = {342--353},
publisher = {Springer},
springer = {http://dx.doi.org/10.1007/3-540-63045-7_35}
}
@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}
}
@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}
}
@phdthesis{Str94PhD,
author = {Tyko Stra{\ss}en},
title = {The Basic Logic of Proofs},
school = {University of Bern},
year = {1994},
month = {April},
pdf = {http://www.strassen.us/thesis.pdf}
}
@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 = {December},
springer = {http://dx.doi.org/10.1007/BF01530789}
}
@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 = {December},
elsevier = {http://dx.doi.org/10.1016/S0168-0072(01)00066-5}
}
@inproceedings{TYav05JLC,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Negative Operations on Proofs and Labels},
booktitle = {Third {M}oscow --- {V}ienna Workshop on {L}ogic and {C}omputation,
{S}teklov Mathematical Institute, {M}oscow, {R}ussia, {M}ay 31--{J}une 1, 2004, Selected Papers},
year = {2005},
editor = {Sergei I. Adian and Matthias Baaz and Lev D. Beklemishev},
volume = {15(4)},
series = {Journal of Logic and Computation},
pages = {517--537},
publisher = {Oxford University Press},
month = {August},
oxford = {http://dx.doi.org/10.1093/logcom/exi026}
}
@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 = {June},
pdf = {http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint239.pdf}
}
@inproceedings{TYav06JLC,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Logic of {P}roofs and Labels with a Complete Set of Operations},
booktitle = {Computer Science Applications of Modal Logic, International Conference,
{M}oscow, {R}ussia, {S}eptember 5--9, 2005, Proceedings},
year = {2006},
editor = {Valentin Shehtman},
volume = {16(5)},
series = {Journal of Logic and Computation},
pages = {697--710},
publisher = {Oxford University Press},
month = {October},
oxford = {http://dx.doi.org/10.1093/logcom/exl032},
conference = {http://www.mccme.ru/ml2005/}
}
@inproceedings{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},
springer = {http://dx.doi.org/10.1007/11753728_38},
conference = {http://logic.pdmi.ras.ru/~csr2006/}
}
@article{TYav08TCS,
author = {Tatiana {Yavorskaya (Sidon)}},
title = {Interacting Explicit Evidence Systems},
journal = {Theory of Computing Systems},
year = {2008},
volume = {43},
number = {2},
pages = {272--293},
month = {August},
springer = {http://dx.doi.org/10.1007/s00224-007-9057-y},
note = {Published online in October 2007}
}
@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},
jancl = {http://dx.doi.org/10.3166/jancl.17.283-316},
pages = {283--316}
}
@inproceedings{RYav02APAL,
author = {Rostislav E. Yavorsky},
title = {Provability logics with quantifiers on proofs},
booktitle = {First {St.~P}etersburg Conference on Days of Logic and Computability,
{M}ay 26--29, 1999, {S}teklov Institute of Mathematics, {St.~P}etersburg, {R}ussia},
year = {2001},
editor = {Yuri [V.] Matiyasevich},
volume = {113(1--3)},
series = {Annals of Pure and Applied Logic},
pages = {373--387},
month = {December},
publisher = {Elsevier},
elsevier = {http://dx.doi.org/10.1016/S0168-0072(01)00067-7},
conference = {http://logic.pdmi.ras.ru/LogicDays},
ps = {http://www.mi.ras.ru/~rey/papers/apal.ps}
}
@inproceedings{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},
springer = {http://dx.doi.org/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}
}
@inproceedings{RYav02AiML,
author = {Rostislav E. Yavorsky},
title = {On Arithmetical Completeness of First-Order Logics of Provability},
booktitle = {Advances in Modal Logic, Third International Workshop,
{AiML} 2000,
{U}niversity of {L}eipzig, {L}eipzig, {G}ermany, {O}ctober 4--7, 2000},
year = {2002},
editor = {Frank Wolter and Heinrich Wansing and Maarten de Rijke and Michael Zakharyaschev},
volume = {3},
series = {Advances in Modal Logic},
pages = {1--16},
publisher = {World Scientific},
conference = {http://www.aiml.net/conferences/aiml-2000/},
ps = {http://www.mi.ras.ru/~rey/papers/aiml2000.ps}
}
@unpublished{RYav03Unp,
author = {R[ostislav] E. Yavorsky},
title = {Undecidability of the minimal provability logic with quantifiers on proofs},
note = {Unpublished},
year = {2003},
month = {November},
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},
pages = {112--124},
mathnet = {http://mi.mathnet.ru/eng/tm410},
russian = {http://www.mi.ras.ru/~rey/papers/prenex.ps}
}
@inproceedings{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},
booktitle = {Third {M}oscow --- {V}ienna Workshop on {L}ogic and {C}omputation,
{S}teklov Mathematical Institute, {M}oscow, {R}ussia, {M}ay 31--{J}une 1, 2004, Selected Papers},
year = {2005},
editor = {Sergei I. Adian and Matthias Baaz and Lev D. Beklemishev},
volume = {15(4)},
series = {Journal of Logic and Computation},
pages = {539--549},
month = {August},
publisher = {Oxford University Press},
oxford = {http://dx.doi.org/10.1093/logcom/exi037}
}
@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 = {June},
pdf = {http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint238.pdf}
}
This file was generated by bibtex2html 1.92.
Compiled by Roman Kuznets, 2008