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.
Financial applications such as Landing and Payment protocols, and their realization
in decentralized financial (DeFi) applications in Blockchains, comprise a unique domain
where bugs in the code may be exploited by anyone to steal assets. This situation
provides unique opportunities for formal verification to enable “move fast and break nothing”.
Formal verification can be used to detect errors early in the development process and
guarantee correctness when a new version of the code is deployed.
I will describe an attempt to automatically verify DeFis and identify potential bugs. The approach is based on breaking the verification of DeFis into decidable verification tasks. Each of these tasks is solved via a decision procedure which automatically generates a formal proof or a test input showing a violation of the specification. In order to overcome undecidability, high level properties are expressed as ghost states and static analysis used to infer how low level programs update ghost states.
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.
Over the recent years deep learning has found successful applications in mathematical reasoning. Today, we can predict fine-grained proof steps, relevant premises, and even useful conjectures using neural networks. This extended abstract summarizes recent developments of machine learning in mathematical reasoning and the vision of the N2Formal group at Google Research to create an automatic mathematician. The second part discusses the key challenges on the road ahead.
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