Formal verification of a proof procedure for the description logic ALC

PorJosé A. Alonso

Se ha publicado un artñiculo de razonamiento formalizado en Isabelle/HOL titulado Formal verification of a proof procedure for the description logic ALC.

Sus autores son

  • Mohamed Chaabani (LIMOSE, Universidad de Boumerdes, Argelia),
  • Mohamed Mezghiche (LIMOSE, Universidad de Boumerdes, Argelia) y
  • Martin Strecker (IRIT (Institut de Recherche en Informatique de Toulouse), Francia)

El trabajo se presentó en el SCSS 2012 (Fourth International Symposium on
Symbolic Computation in Software Science), cuyas actas se publicaron la semana pasada.

Su resumen es

Description Logics (DLs) are a family of languages used for the representation and reasoning on the knowledge of an application domain, in a structured and formal manner. In order to achieve this objective, several provers, such as RACER and FaCT++, have been implemented, but these provers themselves have not been yet certified. In order to ensure the soundness of derivations in these DLs, it is necessary to formally verify the deductions applied by these reasoners. Formal methods offer powerful tools for the specification and verification of proof procedures, among them there are methods for proving properties such as soundness, completeness and termination of a proof procedure. In this paper, we present the definition of a proof procedure for the Description Logic ALC, based on a semantic tableau method. We ensure validity of our prover by proving its soundness, completeness and termination properties using Isabelle proof assistant. The proof proceeds in two phases, first by establishing these properties on an abstract level, and then by instantiating them for an implementation based on lists.

En el 2007 presentamos una formalización análoga en PVS: A formally verified prover for the ALC description logic.

Pratt’s primality certificates

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Pratt’s primality certificates.

Su autores son Simon Wimmer y Lars Noschinski (Technische Universität München).

El artículo se ha publicado el 22 de julio en el Archive of Formal Proofs.

Su resumen es

In 1975, Pratt introduced a proof system for certifying primes. He showed that a number p is prime iff a primality certificate for p exists. By showing a logarithmic upper bound on the length of the certificates in size of the prime number, he concluded that the decision problem for prime numbers is in NP. This work formalizes soundness and completeness of Pratt’s proof system as well as an upper bound for the size of the certificate.

Reseña: Program verification based on Kleene algebra in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Program verification based on Kleene algebra in Isabelle/HOL.

Sus autores son Alasdair Armstrong, Georg Struth y Tjark Weber (los dos primeros de la Universidad de Sheffield y el tercero de la de Uppsala).

El trabajo se ha presentado esta semana en el ITP 2013 (4th Conference on
Interactive Theorem Proving).

Su resumen es

Schematic Kleene algebra with tests (SKAT) supports the equational verification of flowchart scheme equivalence and captures simple while programs with assignment statements. We formalise SKAT in Isabelle/HOL, using the quotient type package to reason equationally in this algebra. We apply this formalisation to a complex flowchart transformation proof from the literature. We extend SKAT with assertion statements and derive the inference rules of Hoare logic. We apply this extension in simple program verification examples and the derivation of additional Hoare-style rules. This shows that algebra can provide an abstract semantic layer from which different program analysis and verification tasks can be implemented in a simple lightweight way.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.

Reseña: “Formalizing bounded increase”

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre terminación titulado Formalizing bounded increase.

Su autor es René Thiemann (de la Univ. de Innsbruck, Austria) y lo presentará en la ITP 2013 (4th International Conference on Interactive Theorem Proving).

Su resumen es

Bounded increase is a termination technique where it is tried to find an argument x of a recursive function that is increased repeatedly until it reaches a bound b, which might be ensured by a condition x < b. Since the predicates like < may be arbitrary user-defined recursive functions, an induction calculus is utilized to prove conditional constraints. In this paper, we present a full formalization of bounded increase in the theorem prover Isabelle/HOL. It fills one large gap in the pen-and-paper proof, and it includes generalized inference rules for the induction calculus as well as variants of the Babylonian algorithm to compute square roots. These algorithms were required to write executable functions which can certify untrusted termination proofs from termination tools that make use of bounded increase. And indeed, the resulting certifier was already useful: it detected an implementation error that remained undetected since 2007.