touistlogo

TouIST

A friendly language for propositional logic and more

forkme

Beyond the Boolean connectives of propositional logic, the input language of TouIST allows sets, conjunctions and disjunctions parametrized by sets, abbreviations You can express complex propositional formulas as

\[\bigwedge_{i\in\{1..9\}} \bigvee_{j\in\{1..9\}}\bigwedge_{n\in\{1..9\}}\bigwedge_{m\in\{1..9\},m\neq n}(p_{i,j,n}\rightarrow \lnot p_{i,j,m}) \]

which translates to:

    bigand $i in [1..9]:
      bigor $j in [1..9]:
        bigand $n,$m in [1..9],[1..9] when $m != $n:
          p($i,$j,$n) => not p(i,j,m)
        end
      end
    end

We can conveniently express and solve problems such as the Sudoku (see example) or finding a winning strategy for the Nim game (Gasquet et al. [3], example).

The team behind TouIST consists of Frédéric Maris (Associate Professor), Olivier Gasquet (Full Professor), Dominique Longin (Research Scientist) and Maël Valais (PhD student) at Institut de Recherche en Informatique de Toulouse (IRIT). It is a “second” or “new” version of a previous program, SAToulouse. TouIST is now actively developed in context of Maël Valais' PhD thesis.

Also, feel free to come to our Gitter chatroom for any request, bug or remarks! Or you can create a ticket on the issue tracker.

screenshot


References

[1]Khaled Skander Ben Slimane, Alexis Comte, Olivier Gasquet, Abdelwahab Heba, Olivier Lezaud, Frédéric Maris, and Maël Valais. “La Logique Facile Avec TouIST (formalisez et Résolvez Facilement Des Problèmes Du Monde Réel).” In Actes Des 9es Journées d’Intelligence Artificielle Fondamentale (IAF 2015). 2015. http://​pfia2015.​inria.​fr/​actes/​download.​php?​conf=​IAF&​file=​Ben_​Slimane_​IAF_​2015.​pdf🔎
[2]Khaled Skander Ben Slimane, Alexis Comte, Olivier Gasquet, Abdelwahab Heba, Olivier Lezaud, Frederic Maris, and Mael Valais. “Twist Your Logic with TouIST.” In Fourth International Conference on Tools for Teaching Logic, TTL   2015, Rennes, France, June 9-12, 2015. Proceedings, edited by Antonia Huertas, João Marcos, María Manzano, Sophie Pinchinat, and François Schwarzentruber, 01–08. Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA). 2015. http://​arxiv.​org/​abs/​1507.​03663🔎
[3]Olivier Gasquet, Andreas Herzig, Dominique Longin, Frédéric Maris, and Maël Valais. “TouIST Again… (Formalisez et Résolvez Facilement Des Problèmes Avec Des Solveurs SAT, SMT et QBF).” In Actes Des 10es Journées d’Intelligence Artificielle Fondamentale (IAF 2017). 2017. https://​www.​irit.​fr/​publis/​LILAC/​Conf_​sans_​actes/​2017_​Gasquet_​et_​al_​IAF.​pdf🔎
[4]Olivier Gasquet, Andreas Herzig, Dominique Longin, Frédéric Maris, and Maël Valais. “La Logique Facile Avec TouIST (poster) (Démonstrations Des Journées Francophones Sur La Planification, La Décision et l’Apprentissage Pour La Conduite de Systèmes, Caen, 06/07/2017-07/07/2017).” 2017. https://​www.​irit.​fr/​publis/​LILAC/​Conf_​sans_​actes/​2017_​Gasquet_​et_​al_​JFPDA-​demonstrations.​pdf🔎