SPRING 2006
CSc 85200.
Seminar in Computational Logic
Code: 94282
Tuesday, 2pm – 4pm, room 3306 (Graduate Center)
May 16 meeting
Speaker: HIDENORI KUROKAWA (Graduate Center)
Topic: Combining Classical and Constructive Logic
In this talk we first present some new results concerning intuitionistic logic with classical atoms (IPCca): Craig interpolation theorem, arithmetical completeness, modal counterparts of IPCca, etc. Then, we compare IPCca with other known approaches to combining classical and constructive logic.
May 9 meeting
Speaker: Yegor Bryukhov (CCNY)
Topic: Matrix-based proof method, part 2.
In this second part of the talk we will try to use an implementation of matrix-based prover in MetaPRL for S4nJ. We’ll try to prove some facts, talk about its performance and the ways of controlling the search space manually. Time permitting, I’ll mention the recent paper of Jens Otten “Clausal Connection-Based Theorem Proving in Intuitionisitc First-Order Logic”, how he performs a dynamic increase of multiplicity and how it can be added to the existing prover in MetaPRL.
May 2 meeting
Speaker: Bryan Renne (Graduate Center)
Topic: Propositional games and explicit strategies
We present a game semantics for the Logic of Proofs, where terms are interpreted as specific strategies on the subformula-choosing evaluation games familiar from propositional (or first-order) logic. Under this interpretation of terms, the LP term operations act as specific operations on strategies. We will close with a discussion of potential interaction with other logic games.
April 25 meeting
There will be 20 min presentations of the members of the Research Laboratory for Logic and Computation (RLLC)
- Yegor Bryukhov. Incorporating decision procedures into proof assistants.
- Bryan Renne. Justifications in formal epistemology.
- Roman Kuznets. Complexity of explicit knowledge.
- Evan Goris. Feasibility of operations on proofs.
- Srikanth Gottipati. Finsler controls.
April 4 meeting
Speaker: Yegor Bryukhov (CCNY)
Topic: Matrix-based prover in MetaPRL
We’ll talk about a matrix-based prover in MetaPRL logical framework:
- Some theory.
- A brief tutorial on how to use the prover for the logic of justified knowledge S4nJ.
- How to prepare a formula manually to achieve a reasonable performance.
- Directions of possible improvements.
- A recent algorithm enhancement by Otten that gives a huge performance boost to matrix-based provers.
I’ll probably need to use two seminars to cover this material.
March 28 meeting
Speaker: Evangelia Antonakos (Graduate Center)
Topic: Justified Knowledge is Usually Sufficient
We will compare the relative strengths of three notions of public knowledge to try to address the observation that the light-weight systems of common knowledge due to McCarthy (`any fool knows’) and Artemov (Justified Knowledge) suffice to solve standard epistemic puzzles for which heavier and more problematic solutions based on Common Knowledge due to Halpern and Moses are offered by standard textbooks. Specifically, we show that Common Knowledge systems are conservative with respect to Justified Knowledge systems on formulas of the form (d & Ja)–>b where a,b,d, are C-free and J-free. These formulas seem to be sufficient to formalize standard epistemic puzzles.
March 21 meeting
Speaker: Melvin Fitting (Lehman/Graduate Center)
Topic: A Replacement Theorem for LP
The replacement theorem for classical and normal modal logics is a fundamental tool. It says that if A and B have been proved equivalent, occurrences of A can be replaced by occurrences of B to produce a formula equivalent to the original one. This theorem does not hold for LP, Logic of Proofs. A replacement to replacement is not easy to formulate. In this talk we provide one, along with some machinery for working with LP realizations that may prove useful for other things as well.
March 14 meeting
Speaker: Bryan Renne (Graduate Center)
Topic: Bisimulation and public announcements in logics of explicit knowledge
We introduce a notion of bisimulation for Fitting models of Artemov’s logics of explicit knowledge. Bisimulation allows us to study the effect of dynamic epistemic operations on language expressivity. It will be shown that public announcements, a basic dynamic epistemic operation, add expressivity to the language of explicit knowledge. It will also be shown that public announcements are definable in the language of explicit knowledge augmented with an explicit evidence accessibility relation.
March 7 meeting
Speaker: Walter Dean (Graduate Center CUNY)
Topic: A Fregean logic of mathematical knowledge (Preliminary report)
In this talk I will present a preliminary attempt to provide a first-order logic of knowledge that is capable of the accommodating fact that otherwise rational agents may be ignorant of various true mathematical statements. I will begin by contrasting three ways by which we might attempt to account for such failures of mathematical omniscience. These can be illustrated by comparing the sense in which we are prepared to accept that any of the following statements can be *false*:
1) i knows that there are infinitely many primes.
2) i knows that Con(PA).
3) i knows that 13! = 6227020800.
The sense in which we allow that 1) can be false can presumably be accounted for by the fact that i can be mathematically competent without explicitly knowing a proof of the infinitude of the primes. Its falsity can therefore be modeled formally by adopting a logic of explicit evidence terms such as that presented in Artemov and Nogina [2005]. The sense in which 2) can be false is presumably to be accounted for in terms of the fact that there are “mathematically possible worlds” compatible with i’s grasp of arithmetic (as given, e.g., by axioms of PA) in which Con(PA) is false. Such failures of mathematical omniscience can thus be accounted for in terms of the familiar Hintikka indistinguishability analysis of the epistemic modality. I will argue that the sense in which we are prepared to regard 3) as false cannot be readily assimilated to either of these approaches. Rather it must be explained in terms of a reading of “i knows that f(a) = b” approximated by “i can compute that f(a) = b.” I will outline an attempt at developing a formal semantics and proof theory for this interpretation of the epistemic modality based on a combination of Fitting’s [2004, 2005] First-Order Intensional Logic, primitive recursive definitions and postive inductive definitions.
February 28 meeting
Speaker: Roman Kuznets (Graduate Center CUNY)
Topic: Epistemic Logics with Justification are decidable
Artemov and Nogina recently introduced explicit knowledge mechanism into several logic of knowledge systems. It was shown that this explicit knowledge is closely connected with the notion of common knowledge. Several systems of epistemic logic with explicit justifications were formulated and given Kripke-style semantics. In this talk we provide the framework that allows to prove decidability of such systems. It turns out that the standard Finite Model Property by itself is not sufficient for proving decidability of these new logics. We show how to generalize the notion of Finite Model Property to achieve the desired result.
February 7 meeting
Speaker: Evan Goris (Graduate Center)
Topic: Realizability in the logic of proofs and formal provability
We will elaborate on the realization theorem for the logic of proofs (LP). Roughly this theorem says that the theorems of S4 are exactly the modal formulas that have explicit counterparts as theorems of LP. The logic of proofs and formal provability (GLA) has potentially more strength than LP in this respect: all theorems of S4 do have explicit counterparts in GLA but there could be more. We will see that this is not so.
This is all part of work in progress. After a general introduction to LP and the realization theorem (depending on the audience) we shall present a proof of the above claim and present two more issues that arise from the proof for which there are no complete answers yet but are probably of more interest.
January 31 meeting
Speaker: Sergei Artemov
Topic: Computer-Aided Proofs and Their Significance
Computer-assisted proofs are playing an increasingly visible role in mathematics. Their scope ranges from routine uses of computational algebra packages to dramatic new discoveries which make newspaper headlines, such as the four-color problem, Kepler’s conjecture, Robbins’ conjecture, etc. Some of these proofs rely heavily upon modules that compute numerical values or decision procedures which do not produce formally certifiable proof codes.
Proof assistants have also reached the stage where they can be used for formalization and certification of real mathematical theorems. Theorems which have been formally verified in this way include the Jordan curve theorem, the prime number theorem, the first G\”odel incompleteness theorem, the aforementioned four-color problem, and other famous mathematical results.
These developments have become possible due to the gradual improvements made by computer scientists in the fields of automated deduction and verification. There are a variety of systems now available ranging from model checkers and fully automated provers for propositional logic to sophisticated proof assistants for higher-order theories; the latter provide user-friendly and theoretically well-founded comprehensive tools for creating, handling, and using formal proofs. Some of these techniques have been used successfully in industry for hardware and software verification. In the formal study of programming languages the state of the art is almost at the point where mechanized metatheoretical tools can be used routinely, and an electronic appendix with machine-checked proofs accompanying papers is fast becoming the norm there.
In this talk we will discuss some methodological and philosophical questions concerning these developments. To what extent can one trust computer-generated proofs? Are such proofs more trustworthy than conventional hand-checked proofs? Can computer proofs be “elegant,” or provide insights about the structure of mathematical objects? Do incompleteness phenomena extend to the foundations of verification? For that matter, can a verifier be verified? What kinds of reflection mechanisms are needed to justify the use of computational and decision procedures in formal proofs? What else should be done to make proof assistance more attractive to users?