The following speakers have accepted to give invited presentations at IJCAR 2024.
Jeremy Avigad, Carnegie Mellon University, USA
Automated Reasoning for Mathematics
Automated reasoning has been around almost as long as computers, and search algorithms and decision procedures were foreshadowed by even earlier results in mathematical logic. Tools like SAT solvers, SMT solvers, and first-order theorem provers have come a long way over the last few decades, and they are becoming increasingly useful for industrial applications. However, the technology has had almost no impact on working mathematicians, even though the tools and methods seem to offer powerful new ways to support mathematical reasoning. This talk will reflect on this state of affairs and consider the role that automated reasoning may play in mathematics in the future.
Laura Kovacs, TU Wien, Austria
Induction in Saturation
One commonly used theory in the development of imperative/functional programs is the theory of inductively defined data types, such as natural numbers, lists and trees. Automating reasoning in formal verification therefore also needs to automate induction. In this talk, we discuss exciting directions in the automation of inductive reasoning, by integrating induction directly into saturation-based proof search. We turn applications of induction into inference rules of the saturation process and add instances of appropriate induction schemata. We propose reasoning methods for strengthening inductive reasoning, handling recursive function definitions and extending inductive reasoning beyond inductively defined data types. Our results show that many problems from formal verification and mathematical theories can now be solved completely automatically using a first-order theorem prover.
Geoff Sutcliffe, University of Miami, USA
Stepping stones in the TPTP World
The first release of the TPTP problem library was made on Friday 12th November 1993. Since then the TPTP World (once gently referred to as the “TPTP Jungle”) has evolved into a well established infrastructure that supports research, development, and deployment of ATP systems. There have been some key developments that helped make the TPTP a success: the CADE ATP System Competition (CASC) that was conceived after CADE-12 in Nancy in 1994, the problem difficulty ratings that were added in 1997, the SZS ontologies that were released in 2004, the addition of Specialist Problem Classes (SPCs) in 2010, and the StarExec service that started in 2013. This talk reviews these and other developments in the TPTP World.