scholarly journals Towards Strong Higher-Order Automation for Fast Interactive Verification

10.29007/3ngx ◽  
2018 ◽  
Author(s):  
Jasmin Christian Blanchette ◽  
Pascal Fontaine ◽  
Stephan Schulz ◽  
Uwe Waldmann

We believe that first-order automatic provers are the best tools available to perform most of the tedious logical work inside proof assistants. From this point of view, it seems desirable to enrich superposition and SMT (satisfiability modulo theories) with higher-order reasoning in a careful manner, to preserve their good properties. Representative benchmarks from the interactive community can guide the design of proof rules and strategies. With higher-order superposition and higher-order SMT in place, highly automatic provers could be built on modern superposition provers and SMT solvers, following a stratified architecture reminiscent of that of modern SMT solvers. We hope that these provers will bring a new level of automation to the users of proof assistants. These challenges and work plan are at the core of the Matryoshka project, funded for five years by the European Research Council. We encourage researchers motivated by the same goals to get in touch with us, subscribe to our mailing list, and join forces.

1994 ◽  
Vol 116 (4) ◽  
pp. 741-750 ◽  
Author(s):  
C. H. Venner

This paper addresses the development of efficient numerical solvers for EHL problems from a rather fundamental point of view. A work-accuracy exchange criterion is derived, that can be interpreted as setting a limit to the price paid in terms of computing time for a solution of a given accuracy. The criterion can serve as a guideline when reviewing or selecting a numerical solver and a discretization. Earlier developed multilevel solvers for the EHL line and circular contact problem are tested against this criterion. This test shows that, to satisfy the criterion a second-order accurate solver is needed for the point contact problem whereas the solver developed earlier used a first-order discretization. This situation arises more often in numerical analysis, i.e., a higher order discretization is desired when a lower order solver already exists. It is explained how in such a case the multigrid methodology provides an easy and straightforward way to obtain the desired higher order of approximation. This higher order is obtained at almost negligible extra work and without loss of stability. The approach was tested out by raising an existing first order multilevel solver for the EHL line contact problem to second order. Subsequently, it was used to obtain a second-order solver for the EHL circular contact problem. Results for both the line and circular contact problem are presented.


10.29007/n6j7 ◽  
2018 ◽  
Author(s):  
Simon Cruanes

We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.


2014 ◽  
Vol 21 (3) ◽  
pp. 401-404
Author(s):  
Dalal A. Maturi ◽  
Antonio J.M. Ferreira ◽  
Ashraf M. Zenkour ◽  
Daoud S. Mashat

AbstractIn this paper, we combine a new higher-order layerwise formulation and collocation with radial basis functions for predicting the static deformations and free vibration behavior of three-layer composite plates. The skins are modeled via a first-order theory, while the core is modeled by a cubic expansion with the thickness coordinate. Through numerical experiments, the numerical accuracy of this strong-form technique for static and vibration problems is discussed.


1995 ◽  
Vol 2 (37) ◽  
Author(s):  
Sten Agerholm ◽  
Mike Gordon

Most general purpose proof assistants support versions of<br />typed higher order logic. Experience has shown that these logics are capable<br />of representing most of the mathematical models needed in Computer<br />Science. However, perhaps there exist applications where ZF-style<br />set theory is more natural, or even necessary. Examples may include<br />Scott's classical inverse-limit construction of a model of the untyped lambda-calculus<br /> (D_inf) and the semantics of parts of the Z specification notation.<br /><br />This paper compares the representation and use of ZF set theory within<br />both HOL and Isabelle. The main case study is the construction of D_inf.<br />The advantages and disadvantages of higher-order set theory versus first-order<br />set theory are explored experimentally. This study also provides a<br />comparison of the proof infrastructure of HOL and Isabelle.


Author(s):  
Christoph Erkinger ◽  
Nysret Musliu

Rotating workforce scheduling (RWS) is an important real-life personnel rostering problem that appears in a large number of different business areas. In this paper, we propose a new exact approach to RWS that exploits the recent advances on Satisfiability Modulo Theories (SMT). While solving can be automated by using a number of so-called SMT-solvers, the most challenging task is to find an efficient formulation of the problem in first-order logic. We propose two new modeling techniques for RWS that encode the problem using formulas over different background theories. The first encoding provides an elegant approach based on linear integer arithmetic. Furthermore, we developed a new formulation based on bitvectors in order to achieve a more compact representation of the constraints and a reduced number of variables. These two modeling approaches were experimentally evaluated on benchmark instances from literature using different state-of-the-art SMT-solvers. Compared to other exact methods, the results of this approach showed an important improvement in the number of found solutions.


Author(s):  
Tomer Libal ◽  
Dale Miller

AbstractUnification is a central operation in constructing a range of computational logic systems based on first-order and higher-order logics. First-order unification has several properties that guide its incorporation in such systems. In particular, first-order unification is decidable, unary, and can be performed on untyped term structures. None of these three properties hold for full higher-order unification: unification is undecidable, unifiers can be incomparable, and term-level typing can dominate the search for unifiers. The so-called pattern subset of higher-order unification was designed to be a small extension to first-order unification that respects the laws governing λ-binding (i.e., the equalities for α, β, and η-conversion) but which also satisfied those three properties. While the pattern fragment of higher-order unification has been used in numerous implemented systems and in various theoretical settings, it is too weak for many applications. This paper defines an extension of pattern unification that should make it more generally applicable, especially in proof assistants that allow for higher-order functions. This extension’s main idea is that the arguments to a higher-order, free variable can be more than just distinct bound variables. In particular, such arguments can be terms constructed from (sufficient numbers of) such bound variables using term constructors and where no argument is a subterm of any other argument. We show that this extension to pattern unification satisfies the three properties mentioned above.


Author(s):  
M. Crampin ◽  
W. Sarlet ◽  
F. Cantrijn

The study of higher-order mechanics, by various geometrical methods, in the framework of the theory of higher-order tangent bundles or jet spaces, has been undertaken by a number of authors recently: for example, Tulczyjew [16, 17], Rodrigues [14, 15] de León [8], Krupka and Musilova [11, and references therein]. In this article we wish to complement these studies by approaching the subject from a new point of view, one which we developed for second-order differential equation fields and first-order Lagrangian mechanics in [19]. In particular, our aim is to show that many of the results we obtained there may be extended to the higher-order case.


2000 ◽  
Vol 417 ◽  
pp. 1-45 ◽  
Author(s):  
YASUHIDE FUKUMOTO ◽  
H. K. MOFFATT

A large-Reynolds-number asymptotic solution of the Navier–Stokes equations is sought for the motion of an axisymmetric vortex ring of small cross-section embedded in a viscous incompressible fluid. In order to take account of the influence of elliptical deformation of the core due to the self-induced strain, the method of matched of matched asymptotic expansions is extended to a higher order in a small parameter ε = (v/Γ)1/2, where v is the kinematic viscosity of fluid and Γ is the circulation. Alternatively, ε is regarded as a measure of the ratio of the core radius to the ring radius, and our scheme is applicable also to the steady inviscid dynamics.We establish a general formula for the translation speed of the ring valid up to third order in ε. This is a natural extension of Fraenkel–Saffman's first-order formula, and reduces, if specialized to a particular distribution of vorticity in an inviscid fluid, to Dyson's third-order formula. Moreover, it is demonstrated, for a ring starting from an infinitely thin circular loop of radius R0, that viscosity acts, at third order, to expand the circles of stagnation points of radii Rs(t) and R˜s(t) relative to the laboratory frame and a comoving frame respectively, and that of peak vorticity of radius R˜p(t) as Rs ≈ R0 + [2 log(4R0/√vt) + 1.4743424] vt/R0, R˜s ≈ R0 + 2.5902739 vt/R0, and Rp ≈ R0 + 4.5902739 vt/R0. The growth of the radial centroid of vorticity, linear in time, is also deduced. The results are compatible with the experimental results of Sallet & Widmayer (1974) and Weigand & Gharib (1997).The procedure of pursuing the higher-order asymptotics provides a clear picture of the dynamics of a curved vortex tube; a vortex ring may be locally regarded as a line of dipoles along the core centreline, with their axes in the propagating direction, subjected to the self-induced flow field. The strength of the dipole depends not only on the curvature but also on the location of the core centre, and therefore should be specified at the initial instant. This specification removes an indeterminacy of the first-order theory. We derive a new asymptotic development of the Biot-Savart law for an arbitrary distribution of vorticity, which makes the non-local induction velocity from the dipoles calculable at third order.


10.29007/k6tp ◽  
2018 ◽  
Author(s):  
Giles Reger ◽  
Nikolaj Bjorner ◽  
Martin Suda ◽  
Andrei Voronkov

This paper introduces a new technique for reasoning with quantifiers and theories. Traditionally, first-order theorem provers (ATPs) are well suited to reasoning with first-order problems containing many quantifiers and satisfiability modulo theories (SMT) solvers are well suited to reasoning with first-order problems in ground theories such as arithmetic. A recent development in first-order theorem proving has been the AVATAR architecture which uses a SAT solver to guide proof search based on a propositional abstraction of the first-order clause space. The approach turns a single proof search into a sequence of proof searches on (much) smaller sub-problems. This work extends the AVATAR approach to use a SMT solver in place of the SAT solver, with the effect that the first-order solver only needs to consider ground-theory-consistent sub-problems. The new architecture has been implemented using the Vampire theorem prover and Z3 SMT solver. Our experimental results, and the results of recent competitions, show that such a combination can be highly effective.


2021 ◽  
Vol Volume 17, Issue 3 ◽  
Author(s):  
Dan Frumin ◽  
Robbert Krebbers ◽  
Lars Birkedal

We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : \tau$, which states that a program $e$ refines a program $e'$ at type $\tau$. ReLoC provides type-directed structural rules and symbolic execution rules in separation-logic style for manipulating the judgment, whereas in prior work on refinements for languages with higher-order state and concurrency, such proofs were carried out by unfolding the judgment into its definition in the model. ReLoC's abstract proof rules make it simpler to carry out refinement proofs, and enable us to generalize the notion of logically atomic specifications to the relational case, which we call logically atomic relational specifications. We build ReLoC on top of the Iris framework for separation logic in Coq, allowing us to leverage features of Iris to prove soundness of ReLoC, and to carry out refinement proofs in ReLoC. We implement tactics for interactive proofs in ReLoC, allowing us to mechanize several case studies in Coq, and thereby demonstrate the practicality of ReLoC. ReLoC Reloaded extends ReLoC (LICS'18) with various technical improvements, a new Coq mechanization, and support for Iris's prophecy variables. The latter allows us to carry out refinement proofs that involve reasoning about the program's future. We also expand ReLoC's notion of logically atomic relational specifications with a new flavor based on the HOCAP pattern by Svendsen et al.


Sign in / Sign up

Export Citation Format

Share Document