December 13 meeting
Speaker:
Evangelia Antonakos (Graduate Center)
Topic:
Fools, Wise Men, and Wives: a look at epistemic logics
introduced by McCarthy et al.
We will go through the formal systems introduced in "On the Modal Theory
of Knowledge" by John McCarthy, Masahiko Sato, Takeshi Hayashi, and
Shigeru Igarashi. In this 1978 paper they introduce the "Any Fool Knows"
modal. We will use this logic to formalize instances of the Wise Men
problem. The "Fool" modality will be shown to be Artemov's "Justified
Knowledge" operator J in the forgetful projection of his LP. We will
also look at McCarthy et. al.'s sound and complete system of a
time-dependent knowledge based logic which models how an agent's
knowledge changes over time while the ground facts remain stable. Within
this framework we will look at instances of the Unfaithful Wives
problem. You may read the paper via a link on McCarthy's site:
http://www-formal.stanford.edu/jmc/model/
December 6 meeting
Speaker:
Hidenori Kurokawa (Graduate Center)
Topic:
Cut-elimination for a Hypersequent Calculus of Intuitionistic
Logic with Classical Atoms
In this paper, we introduce a hypersequent calculus for
intuitionistic logic with classical atoms, i.e. intuitionistic logic
augmented with a special class of propositional variables for which we
postulate the decidability property. This system combines classical
logical reasoning with constructive and computationally oriented
intuitionistic logic in one system. Our main result is the
cut-elimination theorem with the subformula property for this system. We
show this by a semantic method, namely via proving the completeness
theorem of the hypersequent calculus without the cut rule. The
cut-elimintation theorem gives a semantic completeness of the system,
finite model property, decidability, and some form of the disjunction
property.
November 22 meeting
Speaker:
Yuqing Tang (CUNY Graduate Center)
Topic:
A Survey on Argumentation Systems
Argumentation systems are a particular group of patterns of inference,
where arguments for and against a certain claim are produced and
evaluated, to test the tenability of the claim [Prakken et al., 2002].
Each claim is assigned a status of undefeated, defeated, or provisional
defeated (Terms may vary for different authors) based on the status of
the corresponding argument which support it. In general, an
argumentation system contains five elements: 1) an underlying logical
language; 2) a definition of an argument (normally it is a proof of the
underlying logic or a set of premises of such a proof); 3) definitions
of conflicts between arguments and of defeat among arguments; 4) a
preference over claims (sentences in the object language) and an induced
preference over arguments (not all systems have it); 4) a definition of
the status of arguments. The statuses of arguments are obtained by
analyzing the defeat relationship among arguments. There are two
status-assignment approaches: the first is the unique-status-assignment
approach, which have two variants: fixed-point definitions and recursive
definitions (by introducing the notion of sub-argument); the second is
the multiple-status-assignment approach, in which the status of an
argument is determined by their status in all the assignments. In this
talk, I will introduce the variants of the above concepts and approaches
in the representative argumentation systems:
- Pollock's defeasible reasoning and his notion of defeasible
enumeration which is corresponding to
2 in the arithmetic
hierarchy and his interest-driven suppositional reasoning;
- Dung's abstract argumentation framework and his notion of acceptability;
- Prakken & Sartor's defeasible argumentation system with defeasible
preference over arguments where the preference might be inconsistent and
is subjected to argue along with argumentation on sentences.
- Some other representative argumentation systems and the dialectical
aspect of argumentation systems if time allows.
I will also give a brief introduction to my intended research topic:
multiagent AI deliberation and planning using argumentation-based dialogues.
November 15 meeting room C198 (mind an unusual venue!)
A joint session with Jonathan Adler and Arnold Koslow's seminar "Possibility"
Speaker:
Isaac Levi (Columbia)
Topic:
The Logic of Full Belief
A hard copy of the paper is available upon request.
November 8 meeting
Speaker:
Evan Goris
Topic:
Logic of proofs for S-1-2
The talk is about the arithmetical interpretation of (the language of)
the Logic of Proofs LP in Buss' bounded arithmetic S-1-2. This
interpretation distinguishes itself most notably from the one for PA by
the fact that we require that the proof polynomials translate to PTIME
computable functions. In 'Logic of proofs for bounded arithmetic' (G,
2005) LP is shown to be complete for this interpretation.
We first give an introduction to bounded arithmetic and the construction
of a proof predicate in S-1-2. Then we formulate the arithmetical
interpretation of LP in S-1-2. As we will see, the PTIME restriction
mentioned above is quite natural. Then we go over the proof of the
arithmetical completeness theorem. We will try to get clear where the
proof of the arithmetical completeness theorem for PA as given in
'Explicit provability and constructive semantics' (Artemov, BSL 2001),
does not straightforwardly transfer to S-1-2.
If time permits, some related questions can be discussed.
November 1 meeting
Speaker:
Florian Lengyel (Graduate Center CUNY)
Topic:
An asymptotically Gosper-summable enumeration formula
A limit probability distribution formula for a class of combinatorial
objects, the almost-injective functions, is stated. The distribution was
derived from the second of two enumeration formulas for the number of
almost-injective functions.
The first enumeration formula is derived from a rational generating
function, due to Richard Stanley. Gosper's algorithm, applied to this
formula, yields a proof that there is no closed-form representation of
the enumeration formula as a finite sum of dissimilar hypergeometric terms.
The second enumeration formula leads to a limit probability distribution
for the almost injective functions; it was derived from a classification
of the almost injective functions, up to a permutation of the domain, by
a regular language L. This formula has two terms. The first is
Gosper-summable and asymptotically equivalent to the enumeration
formula. It corresponds to a regular monoid contained in L. The second
term is not Gosper summable, but it is asymptotically negligible.
Computer experiments suggest that certain functions classified by
regular monoids have Gosper-summable enumeration formulas.
An introduction to Gosper's algorithm will be given.
October 25 meeting
Speaker:
Bryan Renne
Topic:
Public announcements in logics of explicit knowledge
A public announcement (PA) is the most primitive dynamic operation on
epistemic models. In a 1989 paper, Plaza showed PAs do not add
expressive power to the multi-agent epistemic logic S5, and his result
works for other epistemic logics too. Baltag, Moss, and Solecki have
shown that when common knowledge is added to many of these logics,
Plaza's result no longer holds. A similar phenomenon occurs for
Artemov's logic of explicit knowledge LP, despite the fact that LP at
first glance seems much simpler than multi-agent epistemic logics with
common knowledge. I will discuss my study of an exact formulation of
PAs in logics containing an LP component along with the relationship
of these combined logics to other known logics with PAs. In addition,
I'll mention a number of results and basic definitions I've ran into
during this study.
October 18 meeting
Speaker:
Yegor Bryukhov
Topic:
Tutorial on automatic proof search for S4nJ logic in MetaPRL
We will see how S4nJ is axiomatized in MetaPRL, we'll use J-prover to
prove several examples automatically, including Wise Men Puzzle, two
formulations of Muddy Children. Everybody is encouraged to prepare
his/her own examples that we could try to prove. Due to a kernel bug in
RedHat Linux on our department server you won't be able to interact with
the prover. Instead, I'll be using my notebook and projector.
September 20 meeting
Speaker:
Yegor Bryukhov
Topic:
Matrix-based proof method
We will learn the main concepts of matrix-based proofs, completeness
theorems (matrix characterization of logical validity) for FO classical
logic (Bibel 81), and S4 (Wallen 87). Then we'll discuss why matrix
proofs could be more efficient for automated proving than other known
proof methods. We'll briefly talk about conversion of matrix proofs to
sequent proofs (Schmitt 95).
We will also describe an extension of matrix proofs for S4 to logic of
justified knowledge S4nJ. Time permitting, we will also talk about the
matrix proofs for the Logic of Proofs LP. The last two proof systems
have been implemented as a Metaprl-based prover.
Correction:
Direct LP-proof search is implemented only as a standalone tableau-based
prover. Matrix characterization of LP is known but haven't been
implemented yet.
September 13 meeting
Speaker:
Evan Goris
September 6 meeting
Mel Fitting will show video of Greece. Athens, Delphi, Epidaurus,
Santorini, and the Moschovakis retirement speech. Film not rated. BYOP
(Bring your own popcorn).
August 30 meeting
First meeting of the CS seminar.
