ToulST, A Teacher-and Student-friendly Language for Propositional Logic And Discrete Mathematics

Olivier Gasquet; Dominique Longin; Emiliano Lorini; Frederic Maris; Pierre Regnier; Sergei Soloviev

Olivier Gasquet IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France
Dominique Longin IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France
Emiliano Lorini IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France
Frederic Maris IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France
Pierre Regnier IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France
Sergei Soloviev IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France

Keywords: SAT solvers, propositional logic, higher order logic, discrete mathematics, user- friendly interface

Abstract

This work deals with logical formalization and problem solving using automated solvers. We present the automatic translator TouIST that provides a simple language to generate logical formulas from a problem description. Our tool allows us to model many static or dynamic combinatorial problems. All this can be very helpful as a teaching support for logics and discrete mathematics. Users will benefit from the regular improvements of SAT, QBF or SMT solvers in order to solve concrete logical and combinatorial problems efficiently, e.g., different classes of planning tasks in Artificial Intelligence.

Author Biographies

Olivier Gasquet, IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France

Full Professor, Olivier.Gasquet@irit.fr

Dominique Longin, IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France

Research Scientist, Dominique.Longin@irit.fr

Emiliano Lorini, IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France

Research Scientist, Emiliano.Lorini@irit.fr

Frederic Maris, IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France

Associate Professor, ´ Frederic.Maris@irit.fr

Pierre Regnier, IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France

Associate Professor, ´ Pierre.Regnier@irit.fr

Sergei Soloviev, IRIT, Universit´e de Toulouse, CNRS, Toulouse INP, UT3 118 route de Narbonne, FR 31062, Toulouse, France

Full Professor, Sergei.Soloviev@irit.fr

References

B. Buss and J. Nordstr¨om, “Proof Complexity and SAT Solving,” in Handbook of Satisfiability, 2nd ed., A. Biere et al., eds, Amsterdam: IOS Press, 2021, ch. 7, pp. 233–350; doi: 10.3233/FAIA200990

G. S. Tseitin, “On the Complexity of Derivation in Propositional Calculus,” in Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, Berlin, Heidelberg: Springer, 1983, pp. 466–483; doi: 10.1007/978-3-642-81955-1_28

Z. Luo and S. Soloviev, “Dependent Event Types,” in Proc. of Logic, Language, Information, and Computation - 24th Int. Workshop, WoLLIC 2017, London, UK, July 18-21, 2017, pp. 216–228; doi: 10.1007/978-3-662-55386-2_15

J. Barwise, “Scenes and other situations,” Journal of Philosophy, vol. 78, no. 7, pp. 369–397, 1981; doi: 10.2307/2026481

D. Kroening and O. Strichman, Decision Procedures — An Algorithmic Point of View, 2nd Ed., Berlin: Springer, 2016; doi: 10.1007/978-3-662-50497-0

A. Biere, “Resolve and Expand,” in Proc. of the 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT’04), Vancouver, BC, Canada, May 10–13, 2004, 2005, pp. 59–70.

H. A. Kautz and B. Selman, “Planning as Satisfiability,” in Proc. of the 10th European Conference on Artificial Intelligence, ECAI-92, Vienna, Austria, August 3–7, 1992, pp. 359–363.

J. Rintanen, “Asymptotically Optimal Encodings of Conformant Planning in QBF,” in Proc. of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22–26, 2007, Vancouver, British Columbia, Canada,, 2007, pp. 1045–1050.

J. Rintanen, “Discretization of Temporal Models with Application to Planning with SMT,” in Proc. of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA., 2015, pp. 3349–3355.

J. Shin and E. Davis, “Processes and continuous change in a SAT-based planner,” Artificial Intelligence, vol. 166, no. 1–2, pp. 194–253, 2005; doi: 10.1016/j.artint.2005.04.001

F. Maris and P. Regnier, “TLP-GP: New Results on Temporally-Expressive Planning Benchmarks,” in ˊProc. of the 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2008), November 3–5, Dayton, Ohio, USA, 2008, vol. 1, pp. 507–514; doi: 10.1109/ICTAI.2008.90

O. Gasquet, D. Longin, F. Mari, P. Regnier, and M. Valais, “Compact Tree Encodings for Planning as QBF,” Inteligencia Artificial (Ibero-American Journal of Artificial Intelligence), vol. 21(62), pp. 103–114, 2018; doi: 10.4114/intartif.vol21iss62pp103-113