Duration Calculus - semantics, undecidability, discrete subset of DC, decidability
Kamal Lodaya
Linear time tense/temporal logic on points, completeness, decidability
Tense logic on intervals, axioms for discrete time:
Dense time, undecidability, difficulties in axiomatization
Expressiveness, Relating points and intervals
Slides
J. P. Mayberry
First Order Logic: through the Model Theory of
Herbrand’s functional forms
- Formal Languages and their Interpretations: Formal first and second order languages.
Interpretations and Tarski's definition of satisfaction. Boolean valuations, Universal validity, satisfiability, and logical consequence.
Functional Forms: Prenex normal forms. Herbrand and Skolem functional forms and their semantic (model theoretic) properties.
Canonical interpretations: Definition. Properties of canonical interpretations. Canonical reducts of interpretations and their properties. Model sets.
Tableau Proofs: Smullyan tableaus, Herbrand-Skolem tableaus. Examples.Tableau proofs. Soundness and discussion of completeness.
Herbrand's Theorem: Model-theoretic and proof- theoretic proofs of the theorem
Foundations of Finitary Arithmetic
Finitary Arithmetic as the Theory of Finite Sets Functional Forms and Herbrand's Theorem
The Logic-Automata Connection
Jan 6 16:30-17:30 Reactive systems and automata
Jan 7 11:00-12:30 NFAs: closure properties and algorithms
Jan 7 16:30-17:30 FO(S, <) and S1S
Jan 9 15:15-16:15 Buchi Elgot theorem
Reference : Languages, Automata and Logic - W.Thomas
Jan 10 16:30-17:30 Infinite behaviours
Arindama Singh
Propositional Logic : Compactness and Completeness Theorems
G. Sivakumar
Automated Reasoning & Applications of Logic in Computer Science