FroCos/TABLEAUX 2015 Tutorials

• The distributed ontology, modeling and specification language (DOL) Networks of theories, languages, and logics (half a day)
  Till Mossakowski (Slides)

  
  There is a diversity of ontology languages in use, among them OWL, RDF, OBO, Common Logic, and F-logic. Related languages such as UML class diagrams, entity-relationship diagrams and object role modelling provide bridges from ontology modelling to applications, e.g. in software engineering and databases. Also in model-driven engineering, there is a diversity of diagrams: UML consists of 15 different diagram types, and SysML provides further types. Finally, in software and hardware specification, a variety of formalisms are in use, like Z, VDM, first-order logic, temporal logic etc.
  Another diversity appears at the level of ontology, model and specification modularity and relations among ontologies, specifications and models. There is ontology matching and alignment, module extraction, interpolation, ontologies linked by bridges, interpretation and refinement, and combination of ontologies, models and specifications.

  The Distributed Ontology, Modeling and Specification Language (DOL) aims at providing a unified metalanguage for handling this diversity. In particular, DOL provides constructs for

  • "as-is" use of ontologies, models and specifications (OMS) formulated (as a logical theory) in a specific ontology, modelling or specification language,
  • OMS formalised in heterogeneous logics,
  • modular OMS,
  • mappings between OMS, and
  • networks of OMS,
  • queries.
  DOL has been submitted as a standard to the Object Management Group (OMG).

  The tutorial introduces syntax and semantics of the DOL language, as well as available examples and available tools.

  
  

• Formal Representation of Inductive and Coinductive Datatypes with Applications to Modelling Tableaux Structures (half a day)
  Andrei Popescu (Slides part 1, part 2)

  
  In the past four years, together with Jasmin Blanchette and Dmitriy Traytel, I have worked on designing and implementing a new datatype specification language for Isabelle/HOL. It captures inductive and coinductive structures that can be arbitrarily nested and also combined with non-free structures such as bounded-cardinality sets and multisets. Moreover, the users can "plug and play" with their own structures of interest. A main motivation for designing this specification language was the ability to formalize definitions and results in proof theory in a direct, non-bureaucratic manner.

  I will describe this specification language and its associated mechanisms (including (co)inductive definitional and proof principles) and illustrate by examples its application to formalizing and reasoning about tableaux concepts such as infinite, flexibly branching proof trees and nested sequents. I will emphasize coinductive datatypes, a powerful abstraction mechanism that is unfortunately still regarded as exotic by many logicians and computer scientists.

  (No knowledge of Isabelle/HOL is required for this tutorial.)

  
  

• Automated Reasoning Building Blocks (Sunday 20th)
  Christoph Weidenbach (Slides part 1, part 2)

  
  For some decidable logic fragments, such as, e.g., propositional logic or propositional logic modulo some decidable theories, the current state-of-the art automated reasoning systems are meanwhile useful in a number of application domains. In some domains, such as, e.g., hardware development, they have become part of best practice processes.

  The tutorial reviews the automated reasoning building blocks that caused the progress of automated reasoning systems in the previous two decades. I compare these to building blocks that turned out to be insignificant. The overall idea of the tutorial is to raise an understanding for the important building blocks of automated reasoning systems in general, for the limitations of today's automated reasoning systems, and for challenges that need to be mastered in order to develop systems beyond the current state-of-the-art.

  With respect to logics I assume a basic understanding (syntax, semantics) of first-order logic. The tutorial considers propositional logic, first-order ground, decidable theories (e.g., linear arithmetic), the Bernays-Schoenfinkel fragment up to first-order logic over some type system.

  With respect to calculi I assume a basic understanding of the concept of a calculus. The tutorial considers DPLL, Tableau, Resolution, CDCL, Superposition and combinations of calculi with theories such as CDCL(T) and SUP(T).

  Important building blocks will be (partial) model assumptions, redundancy, orderings on various levels, implementation techniques, and modeling techniques.

  
  

• A Taste of CVC4 (half a day)
  Cesare Tinelli, Andrew Reynolds, Clark Barrett (Slides part 1, part 2)

  
  CVC4 is a versatile solver for Satisfiability Modulo Theories (SMT) with a large user base in both academia and industry. The goal of this tutorial is to give participants a brief overview of SMT, describe the main features of CVC4, and go through a few examples demonstrating how it can be used to solve problems from a variety of applications. We will provide an overview of CVC4's architecture and a detailed description of various aspects of CVC4's internals, including some of its theory solvers, its quantifier reasoning module, and its finite model finder. Participants are expected only to have a basic knowledge of logic and automated deduction. This tutorial will give them a taste of how to encode complex, real-world problems in SMT and effectively use CVC4 to solve them. They will acquire some knowledge of the main components of a modern SMT solver and how they are combined together. They will also get an appreciation of some of the practical issues that arise in using SMT solvers. CVC4, jointly developed at New York University and the University of Iowa, is freely available for both research and commercial use under a liberal open-source license. The presenters of this tutorial are members of the CVC4 development team and have extensive expertise in the foundations and practice of SMT.