FALL 2005
CSc 85200.
Seminar in Computational Logic
Code: 92321
Tuesday, 2pm – 4pm, room 3305 (Graduate Center)
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: https://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.