Search

We present constructive arithmetic in Deduction modulo with rewrite rules only.

Lattice networks are indispensable to study heterogeneous materials such as concrete or rock as well as textiles and woven fabrics. Due to the discrete character of lattices, they quickly become computationally intensive. The QuasiContinuum (QC) Method resolves this challenge by interpolating the displacement of the underlying lattice with a coarser finite element mesh and sampling strategies to accelerate the assembly of the resulting system of governing equations. In lattices with complex heterogeneous microstructures with a high number of randomly shaped inclusions the QC leads to an almost fully-resolved system due to the many interfaces. In the present study the QC Method is expanded with enrichment strategies from the eXtended Finite Element Method (XFEM) to resolve material interfaces using nonconforming meshes. The goal of this contribution is to bridge this gap and improve the computational efficiency of the method. To this end, four different enrichment strategies are compared in terms of their accuracy and convergence behavior. These include the Heaviside, absolute value, modified absolute value and the corrected XFEM enrichment. It is shown that the Heaviside enrichment is the most accurate and straightforward to implement. A first-order interaction based summation rule is applied and adapted for the extended QC for elements intersected by a material interface to complement the Heaviside enrichment. The developed methodology is demonstrated by three numerical examples in comparison with the standard QC and the full solution. The extended QC is also able to predict the results with 5 percent error compared to the full solution, while employing almost one order of magnitude fewer degrees of freedom than the standard QC and even more compared to the fully-resolved system., Comment: 36 pages, 20 figures

The smallest transitive relation < on well-typed normal terms such that if t is a strict subterm of u then t < u and if T is the normal form of the type of t and the term t is not a sort then T < t is well-founded in the type systems of the cube. Thus every term admits a eta-long normal form.

If the sequent (Gamma entails forall x exists y A) is provable in first order constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A), where f is a new function symbol, is a conservative extension of Gamma.

We explore the features of a user interface where formal proofs can be built through gestural actions. In particular, we show how proof construction steps can be associated to drag-and-drop actions. We argue that this can provide quick and intuitive proof construction steps. This work builds on theoretical tools coming from deep inference. It also resumes and integrates some ideas of the former proof-by-pointing project.

We present a formally verified global optimization framework. Given a semialgebraic or transcendental function $f$ and a compact semialgebraic domain $K$, we use the nonlinear maxplus template approximation algorithm to provide a certified lower bound of $f$ over $K$. This method allows to bound in a modular way some of the constituents of $f$ by suprema of quadratic forms with a well chosen curvature. Thus, we reduce the initial goal to a hierarchy of semialgebraic optimization problems, solved by sums of squares relaxations. Our implementation tool interleaves semialgebraic approximations with sums of squares witnesses to form certificates. It is interfaced with Coq and thus benefits from the trusted arithmetic available inside the proof assistant. This feature is used to produce, from the certificates, both valid underestimators and lower bounds for each approximated constituent. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of multivariate transcendental inequalities. We illustrate the performance of our formal framework on some of these inequalities as well as on examples from the global optimization literature., Comment: 24 pages, 2 figures, 3 tables

We consider the problem of certifying lower bounds for real-valued multivariate transcendental functions. The functions we are dealing with are nonlinear and involve semialgebraic operations as well as some transcendental functions like $\cos$, $\arctan$, $\exp$, etc. Our general framework is to use different approximation methods to relax the original problem into polynomial optimization problems, which we solve by sparse sums of squares relaxations. In particular, we combine the ideas of the maxplus estimators (originally introduced in optimal control) and of the linear templates (originally introduced in static analysis by abstract interpretation). The nonlinear templates control the complexity of the semialgebraic relaxations at the price of coarsening the maxplus approximations. In that way, we arrive at a new - template based - certified global optimization method, which exploits both the precision of sums of squares relaxations and the scalability of abstraction methods. We analyze the performance of the method on problems from the global optimization literature, as well as medium-size inequalities issued from the Flyspeck project., Comment: 27 pages, 3 figures, 4 tables

We consider the problem of self tolerance in the frame of a minimalistic model of the idiotypic network. A node of this network represents a population of B lymphocytes of the same idiotype which is encoded by a bit string. The links of the network connect nodes with (nearly) complementary strings. The population of a node survives if the number of occupied neighbours is not too small and not too large. There is an influx of lymphocytes with random idiotype from the bone marrow. Previous investigations have shown that this system evolves toward highly organized architectures, where the nodes can be classified into groups according to their statistical properties. The building principles of these architectures can be analytically described and the statistical results of simulations agree very well with results of a modular mean field theory. In this paper we present simulation results for the case that one or several nodes, playing the role of self, are permanently occupied. We observe that the group structure of the architecture is very similar to the case without self antigen, but organized such that the neighbours of the self are only weakly occupied, thus providing self tolerance. We also treat this situation in mean field theory which give results in good agreement with data from simulation., Comment: 7 pages, 6 figures, 1 table

We consider the problem of certifying an inequality of the form $f(x)\geq 0$, $\forall x\in K$, where $f$ is a multivariate transcendental function, and $K$ is a compact semialgebraic set. We introduce a certification method, combining semialgebraic optimization and max-plus approximation. We assume that $f$ is given by a syntaxic tree, the constituents of which involve semialgebraic operations as well as some transcendental functions like $\cos$, $\sin$, $\exp$, etc. We bound some of these constituents by suprema or infima of quadratic forms (max-plus approximation method, initially introduced in optimal control), leading to semialgebraic optimization problems which we solve by semidefinite relaxations. The max-plus approximation is iteratively refined and combined with branch and bound techniques to reduce the relaxation gap. Illustrative examples of application of this algorithm are provided, explaining how we solved tight inequalities issued from the Flyspeck project (one of the main purposes of which is to certify numerical inequalities used in the proof of the Kepler conjecture by Thomas Hales)., Comment: 7 pages, 3 figures, 3 tables, Appears in the Proceedings of the European Control Conference ECC'13, July 17-19, 2013, Zurich, pp. 2244--2250, copyright EUCA 2013

The aim of this work is to certify lower bounds for real-valued multivariate functions, defined by semialgebraic or transcendental expressions. The certificate must be, eventually, formally provable in a proof system such as Coq. The application range for such a tool is widespread; for instance Hales' proof of Kepler's conjecture yields thousands of inequalities. We introduce an approximation algorithm, which combines ideas of the max-plus basis method (in optimal control) and of the linear templates method developed by Manna et al. (in static analysis). This algorithm consists in bounding some of the constituents of the function by suprema of quadratic forms with a well chosen curvature. This leads to semialgebraic optimization problems, solved by sum-of-squares relaxations. Templates limit the blow up of these relaxations at the price of coarsening the approximation. We illustrate the efficiency of our framework with various examples from the literature and discuss the interfacing with Coq., Comment: 16 pages, 3 figures, 2 tables

We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's trace encoding which is universally defined for any function type, regardless of being impredicative. Direct and concrete interpretations of simultaneous induction and mutually recursive functions are also provided by extending Dybjer's interpretations on the basis of Aczel's rule sets. Our model can be regarded as a higher-order generalization of the truth-table methods. We provide a relatively simple consistency proof of type theory, which can be used as the basis for a theorem prover.

We present a type theory with some proof-irrelevance built into the conversion rule. We argue that this feature is useful when type theory is used as the logical formalism underlying a theorem prover. We also show a close relation with the subset types of the theory of PVS. We show that in these theories, because of the additional extentionality, the axiom of choice implies the decidability of equality, that is, almost classical logic. Finally we describe a simple set-theoretic semantics., Comment: 20 pages, Logical Methods in Computer Science, Long version of IJCAR 2006 paper