The Imandra Automated Reasoning System (system description)
Imandra Inc.（Imandra公司）
Grant Olney Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, Nicola Mometto
备注：
To appear in Proceedings of The International Joint Conference on Automated Reasoning (IJCAR) 2020, Lecture Notes in Artificial Intelligence, Springer-Verlag
We describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision procedures such as SMT, semi-automatic inductive provers of the Boyer-Moore family like ACL2, and interactive proof assistants for typed higher-order logics. Imandra's logic is computational, based on a pure subset of OCaml in which all functions are terminating, with restrictions on types and higher-order functions that allow conjectures to be translated into multi-sorted first-order logic with theories, including arithmetic and datatypes. Imandra has novel features supporting large-scale industrial applications, including a seamless integration of bounded and unbounded verification, first-class computable counterexamples, efficiently executable models and a cloud-native architecture supporting live multiuser collaboration.
The core reasoning mechanisms of Imandra are (i) a semi-complete procedure for finding models of formulas in the logic mentioned above, centered around the lazy expansion of recursive functions, and (ii) an inductive waterfall and simplifier which "lifts" many Boyer-Moore ideas to our typed higher-order setting.
These mechanisms are tightly integrated and subject to many forms of user control. Imandra's user interfaces include an interactive toplevel, Jupyter notebooks and asynchronous document-based verification (in the spirit of Isabelle's Prover IDE) with VS Code.
Institute for Computing and Information Sciences（计算与信息科学研究所）；Radboud University Nijmegen（拉德堡德大学奈梅亨分校）
Requirements about the quality of clinical guidelines can be represented by schemata borrowed from the theory of abductive diagnosis, using temporal logic to model the time-oriented aspects expressed in a guideline. Previously, we have shown that these requirements can be verified using interactive theorem proving techniques. In this paper, we investigate how this approach can be mapped to the facilities of a resolution-based theorem prover, Otter, and a complementary program that searches for finite models of first-order statements, Mace. It is shown that the reasoning required for checking t…
This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and highly interactive setting for discussions around the following four topics. Implementation and development of proof assistants based on any notion of impredicativity, automated theorem proving tools for higher-order logic reasoning systems, logical framework technology for the representation of proofs in higher-order logic, formal digital libraries for storing, maintaining and querying databases of proofs. We envisi…
Universität Koblenz-Landau（科布伦茨-兰道大学）；Harz University of Applied Sciences（哈尔茨应用科学大学）
Deontic logic is a very well researched branch of mathematical logic and philosophy. Various kinds of deontic logics are considered for different application domains like argumentation theory, legal reasoning, and acts in multi-agent systems. In this paper, we show how standard deontic logic can be used to model ethical codes for multi-agent systems. Furthermore we show how Hyper, a high performance theorem prover, can be used to prove properties of these ethical codes.
Learning Guided Automated Reasoning: A Brief Survey
Czech Technical University in Prague（捷克技术大学布拉格）；Radboud University Nijmegen（拉德堡德大学奈杰姆）；Czech Academy of Sciences Institute for Computer Science（捷克科学院计算机科学研究所）；University of Innsbruck（因斯布鲁克大学）
University of Innsbruck（因斯布鲁克大学）；Radboud University Nijmegen（拉德堡德大学奈梅亨分校）
Machine Learner for Automated Reasoning (MaLARea) is a learning and reasoning system for proving in large formal libraries where thousands of theorems are available when attacking a new conjecture, and a large number of related problems and proofs can be used to learn specific theorem-proving knowledge. The last version of the system has by a large margin won the 2013 CASC LTB competition. This paper describes the motivation behind the methods used in MaLARea, discusses the general approach and the issues arising in evaluation of such system, and describes the Mizar@Turing100 and CASC'24 versi…
These are the post-proceedings of the second ARCADE workshop, which took place on the 26th August 2019 in Natal, Brazil, colocated with CADE-27. ARCADE stands for Automated Reasoning: Challenges, Applications, Directions, Exemplary achievements. The goal of this workshop was to bring together key people from various sub-communities of automated reasoning--such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving---to discuss the present, past, and future of the field.
The likelihood of an automated reasoning program being of substantial assistance for a wide spectrum of applications rests with the nature of the options and parameters it offers on which to base needed strategies and methodologies. This article focuses on such a spectrum, featuring W. McCune's program OTTER, discussing widely varied successes in answering open questions, and touching on some of the strategies and methodologies that played a key role. The applications include finding a first proof, discovering single axioms, locating improved axiom systems, and simplifying existing proofs. The…
We present the Theorem Prover Museum, and initiative to conserve -- and make publicly available -- the sources and source-related artefacts of automated reasoning systems. Theorem provers have been at the forefront of Artificial Intelligence, stretching the limits of computation, and incubating many innovations we take for granted today. Without the systems themselves as preserved cultural artefacts, future historians will have difficulties to study the history of science and engineering in our discipline.
This note reports on some experiments, using a handful of standard automated reasoning tools, for exploring Steinitz-Rademacher polyhedra, which are models of a certain first-order theory of incidence structures. This theory and its models, even simple ones, presents significant, geometrically fascinating challenges for automated reasoning tools.
In the last two decades, modal and description logics have been applied to numerous areas of computer science, including knowledge representation, formal verification, database theory, distributed computing and, more recently, semantic web and ontologies. For this reason, the problem of automated reasoning in modal and description logics has been thoroughly investigated. In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic K(m), and of its notational variant, the description logic ALC. Although simple in structure, K(m)/AL…
Our objective in this note is to comment briefly on the newly emerging literature on computer-aided proofs in Social Choice Theory. We shall specifically comment on two papers, one by Tang and Lin (2009) and another by Geist and Endriss (2011). We also provide statements and brief descriptions of the results discussed in this note.
We propose a new graph-based spatial temporal logic for knowledge representation and automated reasoning in this paper. The proposed logic achieves a balance between expressiveness and tractability in applications such as cognitive robots. The satisfiability of the proposed logic is decidable. We apply a Hilbert style axiomatization for the proposed graph-based spatial temporal logic, in which Modus ponens and IRR are the inference rules. We show that the corresponding deduction system is sound and complete and can be implemented through SAT.
This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the logically complex parts of software. The talk will first present how computer algebra methods, such as Groebner basis computation, quantifier elimination and algebraic recurrence solving, help us in inferring properties of program loops with non-trivial arithmetic. Typical properties inferred by our work are loop invariants and expressions bounding the numbe…
University of Innsbruck（因斯布鲁克大学）；Czech Technical Univ. in Prague（布拉格捷克理工大学）
Automated reasoning and theorem proving have recently become major challenges for machine learning. In other domains, representations that are able to abstract over unimportant transformations, such as abstraction over translations and rotations in vision, are becoming more common. Standard methods of embedding mathematical formulas for learning theorem proving are however yet unable to handle many important transformations. In particular, embedding previously unseen labels, that often arise in definitional encodings and in Skolemization, has been very weak so far. Similar problems appear when…
Driving an automobile involves the tasks of observing surroundings, then making a driving decision based on these observations (steer, brake, coast, etc.). In autonomous driving, all these tasks have to be automated. Autonomous driving technology thus far has relied primarily on machine learning techniques. We argue that appropriate technology should be used for the appropriate task. That is, while machine learning technology is good for observing and automatically understanding the surroundings of an automobile, driving decisions are better automated via commonsense reasoning rather than mach…
We introduce an intuitive algorithmic methodology for enacting automated rewriting of string diagrams within a general double-pushout (DPO) framework, in which the sequence of rewrites is chosen in accordance with the causal structure of the underlying diagrammatic calculus. The combination of the rewriting structure and the causal structure may be elegantly formulated as a weak 2-category equipped with both total and partial monoidal bifunctors, thus providing a categorical semantics for the full multiway evolution causal graph of a generic Wolfram model hypergraph rewriting system. As an ill…
University of Bamberg（班贝格大学）；Freie Universität Berlin（柏林自由大学）；Université du Luxembourg（卢森堡大学）
The logico-pluralist LogiKEy knowledge engineering methodology and framework is applied to the modelling of a theory of legal balancing in which legal knowledge (cases and laws) is encoded by utilising context-dependent value preferences. The theory obtained is then used to formalise, automatically evaluate, and reconstruct illustrative property law cases (involving appropriation of wild animals) within the Isabelle proof assistant system, illustrating how LogiKEy can harness interactive and automated theorem proving technology to provide a testbed for the development and formal verification o…
The development of safety-critical systems requires the control of hazards that can potentially cause harm. To this end, safety engineers rely during the development phase on architectural solutions, called safety patterns, such as safety monitors, voters, and watchdogs. The goal of these patterns is to control (identified) faults that can trigger hazards. Safety patterns can control such faults by e.g., increasing the redundancy of the system. Currently, the reasoning of which pattern to use at which part of the target system to control which hazard is documented mostly in textual form or by …
Robert Bosch GmbH（罗伯特·博世有限公司）；RWTH Aachen（亚琛工业大学）；ika（ika（亚琛工业大学汽车研究所））
Knowledge representation and reasoning has a long history of examining how knowledge can be formalized, interpreted, and semantically analyzed by machines. In the area of automated vehicles, recent advances suggest the ability to formalize and leverage relevant knowledge as a key enabler in handling the inherently open and complex context of the traffic world. This paper demonstrates ontologies to be a powerful tool for a) modeling and formalization of and b) reasoning about factors associated with criticality in the environment of automated vehicles. For this, we leverage the well-known 6-Lay…
University of Innsbruck（因斯布鲁克大学）；Radboud University（拉德堡德大学）
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the proofs, producing an AI system capable of answering a wide range of mathematical queries automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39% of the 14185 theorems could be proved in a push-button mode (without any high-…
Freie Universität Berlin（柏林自由大学）；Cambridge University（剑桥大学）
We present an automated verification of the well-known modal logic cube in Isabelle/HOL, in which we prove the inclusion relations between the cube's logics using automated reasoning tools. Prior work addresses this problem but without restriction to the modal logic cube, and using encodings in first-order logic in combination with first-order automated theorem provers. In contrast, our solution is more elegant, transparent and effective. It employs an embedding of quantified modal logic in classical higher-order logic. Automated reasoning tools, such as Sledgehammer with LEO-II, Satallax and …
Towards an Automated Reasoning Tool for Complexity Analysis of Automated Reasoners
Universidad Politécnica de Madrid (UPM)（马德里理工大学）；IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）；Computer Science Laboratory of Sorbonne University (LIP6)（索邦大学计算机科学实验室）；STMicroelectronics（意法半导体）
The Multi-valued Action Reasoning System (MARS) is an automated value-based ethical decision-making model for artificial agents (AI). Given a set of available actions and an underlying moral paradigm, by employing MARS one can identify the ethically preferred action. It can be used to implement and model different ethical theories, different moral paradigms, as well as combinations of such, in the context of automated practical reasoning and normative decision analysis. It can also be used to model moral dilemmas and discover the moral paradigms that result in the desired outcomes therein. In …
Formally reasoning about functional programs is supposed to be straightforward and elegant, however, it is not typically done as a matter of course. Reasoning in a proof assistant requires "reimplementing" the code in those tools, which is far from trivial. SMLtoCoq provides an automatic translation of SML programs and function contracts into Coq. Programs are translated into Coq specifications, and function contracts into theorems, which can then be formally proved. Using the Equations plugin and other well established Coq libraries, SMLtoCoq is able to translate SML programs without side-eff…
Formal verification of cyber-physical and robotic systems requires that we can accurately model physical quantities that exist in the real-world. The use of explicit units in such quantities can allow a higher degree of rigour, since we can ensure compatibility of quantities in calculations. At the same time, improper use of units can be a barrier to safety and therefore it is highly desirable to have automated sanity checking in physical calculations. In this paper, we contribute a mechanisation of the International System of Quantities (ISQ) and the associated SI unit system in Isabelle/HOL.…
In this paper we investigate further the tableaux system for a deontic action logic we presented in previous work. This tableaux system uses atoms (of a given boolean algebra of action terms) as labels of formulae, this allows us to embrace parallel execution of actions and action complement, two action operators that may present difficulties in their treatment. One of the restrictions of this logic is that it uses vocabularies with a finite number of actions. In this article we prove that this restriction does not affect the coherence of the deduction system; in other words, we prove that the…
Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our framework models concurrent programs as succinct automata and supports the verification of multiple important properties. Safety verification and simulations of succinct automata are parallel compositional, and safety properties of succinct automata are preserved under refinements. We generate succinct automata from infinite state concurrent programs in an automat…
Intensional sets, i.e., sets given by a property rather than by enumerating elements, are widely recognized as a key feature to describe complex problems (see, e.g., specification languages such as B and Z). Notwithstanding, very few tools exist supporting high-level automated reasoning on general formulas involving intensional sets. In this paper we present a decision procedure for a first-order logic language offering both extensional and (a restricted form of) intensional sets (RIS). RIS are introduced as first-class citizens of the language and set-theoretical operators on RIS are dealt wi…
DFKI（德国人工智能研究中心）；U Coimbra（科英布拉大学）；University of Edinburgh（爱丁堡大学）；FU Berlin（柏林自由大学）；Stanford（斯坦福大学）；INRIA Sophia-Antipolis（法国国家信息与自动化研究所索菲亚-安提波利斯分部）
The UITP workshop series brings together researchers interested in designing, developing and evaluating user interfaces for automated reasoning tools, such as interactive proof assistants, automated theorem provers, model finders, tools for formal methods, and tools for visualising and manipulating logical formulas and proofs. The twelth edition of UITP took place in Coimbra, Portugal, and was part of the International Joint Conference on Automated Reasoning (IJCAR'16). The workshop consisted of an invited talk, six presentations of submitted papers and lively hands-on session for reasoning to…
The aim of this PhD project is to develop fast and robust reasoning tools for dependency quantified Boolean formulas (DQBF). In this paper, we outline two properties, autarkies and symmetries, that potentially can be exploited for pre- and in-processing in the DQBF solving process. DQBF extend quantified Boolean formulas (QBF) with non-linear dependencies between the quantified variables. Automated testing and debugging techniques are an essential part of the solvers tool-chain. For rigorous DQBF solver development, we are working on novel automated testing and debugging techniques as successf…
I introduce an approach for automated reasoning in first order set theories that are not finitely axiomatizable, such as $ZFC$, and describe its implementation alongside the automated theorem proving software E. I then compare the results of proof search in the class based set theory $NBG$ with those of $ZFC$.
Pecan is an automated theorem prover for reasoning about properties of Sturmian words, an important object in the field of combinatorics on words. It is capable of efficiently proving non-trivial mathematical theorems about all Sturmian words.
Automated Tactics for Polynomial Reasoning in Lean 4
State Key Laboratory of Mathematical Sciences, Academy of Mathematics and Systems Science, University of Chinese Academy of Science（中国科学院数学与系统科学研究院）；Institute of Logic and Cognition, Department of Philosophy, Sun Yat-sen University（中山大学哲学系逻辑与认知研究所）
This dissertation explores the roles of polarities and focussing in various aspects of Computational Logic. These concepts play a key role in the the interpretation of proofs as programs, a.k.a. the Curry-Howard correspondence, in the context of classical logic. Arising from linear logic, they allow the construction of meaningful semantics for cut-elimination in classical logic, some of which relate to the Call-by-Name and Call-by-Value disciplines of functional programming. The first part of this dissertation provides an introduction to these interpretations, highlighting the roles of polarit…
The sequent calculus is a formalism for proving validity of statements formulated in First-Order Logic. It is routinely used in computer science modules on mathematical logic. Formal proofs in the sequent calculus are finite trees obtained by successively applying proof rules to formulas, thus simplifying them step-by-step. Students often struggle with the mathematical formalities and the level of abstraction that topics like formal logic and formal proofs involve. The difficulties can be categorised as syntactic or semantic. On the syntactic level, students need to understand what a correctly…
