Abstract Modal logics extend classical first-order logic with the modalities of necessity ( $$\Box $$ □ ) and possibility ( $$\Diamond $$ ◊ ). A model of a set of modal logic formulae can be represented by a Kripke structure. This paper describes a method and implementation for finding finite Kripke models for formulae in first-order modal logics. The approach relies on translating the modal logic formulae to classical logic formulae, using an SMT solver to generate a finite model of the classical logic formulae, then translating the classical model to a finite Kripke model. This process has been implemented in the new model finding system MoMo which produces TPTP-compliant Kripke model representations. An evaluation on the modal logic problems in the TPTP problem library confirms the practicality of this approach. Up to the authors’ knowledge, MoMo is the first model finder for first-order modal logics.

Abstract The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. There are key components that help make the TPTP World a success: the TPTP problem library was first released in 1993, the CADE ATP System Competition (CASC) was conceived after CADE-12 in 1994, problem difficulty ratings were added in 1997, the current TPTP language was adopted in 2003, the SZS ontologies were specified in 2004, the TSTP solution library was built starting around 2005, the Specialist Problem Classes (SPCs) have been used to classify problems since 2010, the SystemOnTPTP service has been offered from 2011, the StarExec service was started in 2013, and a world of TPTP users have helped all along. This paper reviews these stepping stones in the development of the TPTP World.

Abstract The TPTP World is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. This work uses data in the TPTP World to assess progress in ATP from 2015 to 2023.

This paper describes a new format for representing Tarskian-style interpretations for formulae in typed first-order logic, using the TPTP TF0 language. It further describes a technique and an implemented tool for verifying models using this representation, and a tool for visualizing interpretations. The research contributes to the advancement of au- tomated reasoning technology for model finding, which has several applications, including verification.

Evaluation of scientific contributions can be done in many different ways. For the various research communities working on the verification of systems (software, hardware, or the underlying involved mechanisms), it is important to bring together the community and to compare the state of the art, in order to identify progress of and new challenges in the research area. Competitions are a suitable way to do that. The first verification competition was created in 1992 (SAT competition), shortly followed by the CASC competition in 1996. Since the year 2000, the number of dedicated verification competitions is steadily increasing. Many of these events now happen regularly, gathering researchers that would like to understand how well their research prototypes work in practice. Scientific results have to be reproducible, and powerful computers are becoming cheaper and cheaper, thus, these competitions are becoming an important means for advancing research in verification technology. TOOLympics 2019 is an event to celebrate the achievements of the various competitions, and to understand their commonalities and differences. This volume is dedicated to the presentation of the 16 competitions that joined TOOLympics as part of the celebration of the $$25^{ th }$$ anniversary of the TACAS conference.