Induction and coinduction are both used extensively within mathematics and computer science. Algebraic formulations of these principles make the duality between them apparent, but do not account well for the way they are commonly used in deduction. Generally, the formalization of these reasoning methods employs inference rules that express a general explicit (co)induction scheme. Non-well-founded proof theory provides an alternative, more robust approach for formalizing implicit (co)inductive reasoning. This approach has been extremely successful in recent years in supporting implicit inductive reasoning, but is not as well-developed in the context of coinductive reasoning. This talk reviews the general method of non-well-founded proofs, and puts forward a concrete natural framework for (co)inductive reasoning, based on (co)closure operators, that offers a concise framework in which inductive and coinductive reasoning are captured as we intuitively understand and use them. Through this framework we demonstrate the enormous potential of non-well-founded deduction, both in the foundational theoretical exploration of (co)inductive reasoning and in the provision of proof support for (co)inductive reasoning within (semi-)automated proof tools.
Bio: Liron Cohen is senior lecturer (assistant professor) in the Department of Computer Science at Ben-Gurion University in Israel. Previously, Liron was a Fulbright postdoctoral researcher at Cornell University working with Robert Constable. She obtained her Ph.D. in 2016 from Tel Aviv University advised by Arnon Avron. Liron's research is motivated by the desire to understand the deep connection between proofs and computation. Her research interests include computer-aided deduction and verification, type systems, logics, programming languages and computational mathematics.
One of the most difficult aspects in formally verifying infinite state systems is reasoning about quantifiers and specifically quantifier altenerations. Indeed alternation cycles lead to divergence and instability of modern SMT solvers. We describe abstractions for preventing cycles and evaluate their effectiveness by verifying tricky distributed protocols. The first abstraction is modularity: break the system into modules and separately verify each module by hiding some dependencies to avoid cycles. The second approach introduces a novel interactive approach to quantifier reasoning using an SMT solver. We automatically abstract the verification condition in a way that eliminates function cycles. The user refines this abstraction in response to spurious counterexamples by proposing ground terms to instantiate quantifiers. In applying this approach to the verification of Byzantine and non-Byzantine fault tolerance protocols, we found that a few manual instantiations were needed. Moreover, the counterexamples provided valuable guidance for the user, in contrast to the timeouts produced by the traditional approach.
Bio: Mooly Sagiv is a professor in the School of Computer Sciences at Tel-Aviv University and a CEO and co-founder of Certora. He is a leading researcher in the area of large scale (inter-procedural) program analysis, and one of the key contributors to shape analysis. His fields of interests include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments.
Bio: Guido Governatori leads the Software Systems Research Group and research activities
on legal informatics at CSIRO's Data61. He received his PhD in Legal Informatics
from the University of Bologna. His research has focused on automated reasoning
techniques for non-classical logic, modal logic and non-monotonic reasoning
(including labelled tableaux for modal logic, rule-based systems, and defeasible logic),
and their applications in the legal domain, autonomous agents and business processes.
Theorem proving with neural networks has made large strides. From using learned heuristics instead of handwritten heuristics, to learning to retrieve premises, to directly predicting proofs using language models; neural networks appear to be surprisingly capable at working with abstract mathematics. This talk gives an overview of recent advances in the field and the paradigms behind them, as well as an outline of the plans of the N2Formal team at Google Research.
Bio: Markus N. Rabe is a software engineer and researcher at Google. He explores the foundations of automated reasoning, including the use of deep learning, and is a member of the N2Formal team, which has the goal to automatically formalize mathematics. Markus has a Ph.D. from Saarland University and visited UC Berkeley as a postdoc.
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret and Petar Vukmirović. Superposition for Full Higher-Order Logic
Visa Nummelin, Alexander Bentkamp, Sophie Tourret and Petar Vukmirović. Superposition with First-Class Booleans and Inprocessing Clausification
Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann and Alisa Kovtunova. Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures
Camillo Fiorentini. Efficient SAT-based proof search in Intuitionistic Propositional Logic
Mnacho Echenim, Radu Iosif and Nicolas Peltier. Unifying Decidable Entailments in Separation Logic with Inductive Definitions
Nicholas Smallbone. Twee: an equational theorem prover (System Description)
Kaustuv Chaudhuri. Subformula Linking for Intuitionistic Logic and Type Theory
Tobias Nipkow and Simon Roßkopf. Isabelle's Metalogic: Formalization and Proof Checker
Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language (System Description)
Ryan Krueger, Jesse Michael Han and Daniel Selsam. Automatically Building Diagrams for Olympiad Geometry Problems (System Description)
Jacob Errington, Junyoung Jang and Brigitte Pientka. Harpoon: Mechanizing Metatheory Interactively (System Description)
Dohan Kim and Christopher Lynch. Equational Theorem Proving Modulo
Martin Suda. New Techniques that Improve ENIGMA-style Clause Selection Guidance
Petra Hozzová, Laura Kovács and Andrei Voronkov. Integer Induction in Saturation
Joanna Golinska-Pilarek, Michal Zawidzki and Taneli Huuskonen. Tableau-based decision procedure for non-Fregean logic of sentential identity
Tanel Tammet, Dirk Draheim and Priit Järv. Confidences for Commonsense Reasoning
Akihisa Yamada. Multi-Dimensional Interpretation Methods for Termination of Term Rewriting
Peter Baumgartner. The Fusemate Logic Programming System (System Description)
Runqing Xu, Liming Li and Bohua Zhan. Verified interactive computation of definite integrals
Filip Bártek and Martin Suda. Neural Precedence Recommender