9th Indian School on Logic and its Applications (ISLA 2022)

(Part-II) (Online)

(July 6-8 & July 20-21, 2022)

In the second volume of ISLA 2022 the following short courses are going to be offered. All the courses are going to be held online.

  1. Descriptive Complexity Theory

    Nikhil Balaji, IIT Delhi (https://sites.google.com/view/nikhilbalaji/home)

    Forenoons (10-12 AM), July 6-8

    The objective of the course is to understand what functions can one compute when one is allowed to use only a constant amount of memory. In a first course on automata theory one learns that finite automata precisely capture such algorithms. We will try to capture a relaxed notion of space used by an algorithm via a model that is a natural generalization of finite automata, and show an example of some surprising algorithms one can design in such a model.

  2. Proofs, Programs & Types

    Piyush P Kurur, IIT Palakkad (https://piyush-kurur.github.io/)

    Afternoons (2:30-4:30 PM), July 6-8

    This is a set of 3 lectures of roughly 2 hrs each where I introduce the participants to writing formal proofs in the proof assistant Coq. Coq belongs to the family of proof assistants that make use of the "propositions as types" principle where the type checking of terms in a (functional) programming language with sufficiently rich type system (dependently typed languages)can double up as proof checking for mathematical statements. This has consequences to both the world of programming and proving.

    1. In Coq we have a programming language where not only can we write interesting programs but also prove their correctness. The programs thus written are called certified programs and hence comes with formal(i.e. machine checked) certificates of correctness.

    2. The Coq proof system and its related IDE gives the mathematician an interactive environment to prove complicated proofs with high assurance in correctness. Domain specific tactics can be designed to automate some of the routine steps in the proofs.

      The lecture is mainly focused on the former, i.e. writing certified proofs however, techniques learned here can also help with the latter.

  3. Description Logics

    Raghava Mutharaju, IIIT Delhi (http://raghavam.github.io)

    Forenoons & Afternoons (10-11 AM, 3-4 PM), July 20-21

    Description Logics (DLs) are a family of formal languages based on first-order logic that are used for knowledge representation and reasoning. They provide the underpinning for the W3C standard named the Web Ontology Language (OWL). OWL is used to build ontologies that can capture the knowledge in a domain in the form of concepts and the relationships between them.

    We will have a series of four lectures where I will discuss the following.

    1. Introduce Description Logics and the various constructs used to capture the knowledge. I will also discuss some of the languages in the DL family. The relationship of DLs with first-order logic and OWL will also be discussed. Introduce OWL, its constructs and four different profiles (OWL 2 EL, OWL 2 QL, OWL 2 RL and OWL 2 DL).
    2. Use Protégé, an open-source IDE, to build an ontology with the help of the participants.

ISLA is a biennial event of the Association of Logic in India (ALI). The details of the last edition of the school can be found here.

Please register here: https://forms.gle/NFVEfxnmayH2Xbh88

Program Committee:

Amaldev Manuel, IIT Goa (amal@iitgoa.ac.in)

Sankha S Basu, IIIT Delhi (sankha@iiitd.ac.in)