TouIST Platform

Heads:  Dominique LONGIN et   Frédéric MARIS

The TouIST platform offers a high-level language for logically modeling various problems in a very compact way using solvers. It consists of: a graphical interface allowing interactive input of the target model; a translation module (compiler) from the input language of TouIST into a language directly understandable by different solvers; a module for viewing models calculated by the solvers. Currently, TouIST can call on three different types of solvers: SAT solvers (propositional logic or logic of predicates on finite domain), QBF (authorizing quantification on propositional formulas), SMT (for the treatment of problems calling on calculations numeric on whole or rational numbers).

The goal of the platform is to allow the user to concentrate on the modeling of a given problem without worrying about the technical details related to the use of solvers: translation of formulas into conjunctive normal form, then translation into language DIMACS, QDIMACS or SMT-LIB (languages ​​used as standard as input to solvers but not very easy to handle directly). TouIST can also be used entirely from the command line for interfacing with intelligent agent architectures capable of reasoning and planning actions: typically for example, checking the validity of an argument, determining the executable actions, checking that a plan is valid or even calculate a complete plan of actions to satisfy a goal, etc.

TouIST is currently used for both teaching and research. In teaching, we use it at the Toulouse 3 University in bachelor’s degree (to present a concrete use of logic in order to model some problems) and in Master (for the modeling of satisfaction problems of constraints and planning). In research, TouIST is an opportunity for permanent research concerning both:

  • the development of its input language where the goal is to obtain a high-level logical language that is as expressive as possible while allowing a translation which remains very compact into the input language of each of the types of usable solver, and by ensuring that the problem translated into this language can be treated as efficiently as possible by the solver considered;
  • extension to other functionalities (extension of the input and output graphical interface, inclusion of plug-ins dedicated to the treatment of specific problems such as, for example, specialized language extensions for problems of argumentation or planning, taking into account modal operators and their translation into classical logic, etc.).

In addition, TouIST is also used within projects of the AI department. For example, in the CoPains ANR project on the development of a persuasive agent for helping the elderly, it is used by the architecture to verify the validity of the conversational action plans of the artificial agent. In addition, the AI department has been developing LoTReC (demonstrator for modal logics) for several years. It is based on a construction of Kripke models based on possible worlds of a modal formula, and is capable of handling potentially any (mono- or multi-) modal logic. Consideration is currently being given to using TouIST to check the consistency of the possible worlds of the models built, which would greatly optimize the execution of LoTReC and considerably reduce certain memory problems inherent in the construction of such models, which are quickly very large.

At the ENS and IRISA in Rennes, Hintikka’s World is a program for visually describing the possible worlds associated with artificial agents (in an epistemic logic approach), and an interfacing module has been developed in order to to make possible the use of TouIST by their program, thanks to which the models to be displayed are calculated in a much more efficient way.

Internationally, TouIST is used in particular by the University of Seville for undergraduate education (following an approach similar to that used at Toulouse 3 University).

Positioning of the platform in relation to existing platforms (local and national)

To our knowledge, there is no equivalent to TouIST in France or elsewhere in the world. Research is focused on the development of the solvers themselves in order to make them as efficient as possible, and not on their usability. Some languages, such as Isabel, allow you to rewrite an interface such as TouIST. The advantage of the latter is to offer a simple, lightweight product that can be used directly for logical modeling, free of rights.

Technical, organizational description, rate of use

TouIST is a command line executable program (developed in OCAML) with a graphical interface (developed in JAVA), the use of which is not compulsory. It currently integrates 3 default solvers (SAT, QBF, SMT) but can interface with any solver taking as input the standard DIMACS, QDIMACS or SMT-LIB languages, which allows TouIST to automatically benefit from the performance of most recent solvers.

The program can be downloaded freely from the web (https://www.irit.fr/touist/), and tutorials have been developed to make it easier to learn. Locally, around 450 students use it each year, in addition to external researchers and teacher-researchers.