Sixth Workshop on Proof eXchange for Theorem Proving

PxTP 2019

Affiliated with the 27th International Conference on Automated Deduction (CADE-27)

26 August 2019, Natal, Brazil

Background

The PxTP workshop brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms.

The progress in computer-aided reasoning, both automatic and interactive, during the past decades, has made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation of such tools in larger verification environments has demonstrated the potential to reduce the amount of manual intervention. Examples include the Sledgehammer tool providing an interface between Isabelle and (untrusted) automated provers, and collaboration of the HOL Light and Isabelle systems in the formal proof of the Kepler conjecture.

Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools for exchanging problems, proofs, and models. The PxTP workshop strives to encourage such cooperation by inviting contributions on suitable integration, translation, and communication methods, standards, protocols, and programming interfaces. The workshop welcomes developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and interfaces, and producers of standards and protocols. We are interested both in success stories and descriptions of current bottlenecks and proposals for improvement

Topics

Topics of interest for this workshop include all aspects of cooperation between reasoning tools, whether automatic or interactive. More specifically, some suggested topics are:

  • applications that integrate reasoning tools (ideally with certification of the result);
  • interoperability of reasoning systems;
  • translations between logics, proof systems, models;
  • distribution of proof obligations among heterogeneous reasoning tools;
  • algorithms and tools for checking and importing (replaying, reconstructing) proofs;
  • proposed formats for expressing problems and solutions for different classes of logic solvers (SAT, SMT, QBF, first-order logic, higher-order logic, typed logic, rewriting, etc.);
  • meta-languages, logical frameworks, communication methods, standards, protocols, and APIs related to problems, proofs, and models;
  • comparison, refactoring, transformation, migration, compression and optimization of proofs;
  • data structures and algorithms for improved proof production in solvers (e.g., efficient proof representations);
  • (universal) libraries, corpora and benchmarks of proofs and theories;
  • alignment of diverse logics, concepts and theories across systems and libraries;
  • engineering aspects of proofs (e.g., granularity, flexiformality, persistence over time);
  • proof certificates;
  • proof checking;
  • mining of (mathematical) information from proofs (e.g., quantifier instantiations, unsat cores, interpolants, ...);
  • reverse engineering and understanding of formal proofs;
  • universality of proofs (i.e. interoperability of proofs between different proof calculi);
  • origins and kinds of proofs (e.g., (in)formal, automatically generated, interactive, ...);
  • Hilbert's 24th Problem (i.e. what makes a proof better than another?);
  • social aspects (e.g., community-wide initiatives related to proofs, cooperation between communities, the future of (formal) proofs);
  • applications relying on importing proofs from automatic theorem provers, such as certified static analysis, proof-carrying code, or certified compilation;
  • application-oriented proof theory;
  • practical experiences, case studies, feasibility studies.
  • Submissions

    Researchers interested in participating are invited to submit either an extended abstract (up to 8 pages) or a regular paper (up to 15 pages). Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. We expect that one author of every accepted paper will present their work at the workshop.

    Submitted papers should describe previously unpublished work, and must be prepared using the LaTeX EPTCS class. Papers should be submitted via EasyChair, at the PxTP'2019 workshop page. Accepted regular papers will appear in an EPTCS volume.

    Important Dates

    Abstract submission: May 12, 2019
    Paper submission: May 19, 2019
    Author notification: June 21, 2019
    Camera ready version due: July 21, 2019
    Workshop: 26 August, 2019

    Invited speakers

    Registration

    Registration to PxTP is handled through CADE registration.

    Proceedings

    The PxTP 2019 proceedings are now available. You can also download a PDF copy.

    Program

    Click on the titles of the talks to download the papers.

    Monday, 26 August 2019

    Chair:Giselle Reis
    9:00-10:00 Invited speaker: Assia Mahboubi

    Systems for Doing Mathematics by Computer

    10:00-10:30 break
    Chair:Haniel Barbosa
    10:30-11:15 Mathias Fleury and Hans-Jörg Schurr

    Reconstructing veriT Proofs in Isabelle/HOL

    11:15-11:45 Mohamed Yacine El Haddad, Guillaume Burel and Frédéric Blanqui

    EKSTRAKTO A tool to reconstruct proofs from TSTP traces in Dedukti

    11:45-12:15 Alex Ozdemir, Aina Niemetz, Mathias Preiner, Yoni Zohar and Clark Barrett

    DRAT-based Bit-Vector Proofs in CVC4

    12:15-14:00 lunch break
    Chair:Stephan Schulz
    14:00-15:00 Invited speaker: Thibault Gauthier

    Learning from Tactic Steps in Formal Proofs

    15:00-15:30 Jieying Chen, Ghadah Abdulrahman S Alghamdi, Renate A. Schmidt, Dirk Walther and Yongsheng Gao

    Modularity Meets Forgetting: A Case Study with the SNOMED CT Ontology

    15:30-16:00 Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett and Cesare Tinelli

    Verifying Bit-vector Invertibility Conditions in Coq

    16:00-16:30 break
    Chair:Cesare Tinelli
    16:30-17:15 Fadil Kallat, Tristan Schäfer and Anna Vasileva

    CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories

    17:15-18:00 Eunice Palmeira Silva, Fred Freitas and Jens Otten

    Converting ALC Connection Proofs into ALC Sequents

    18:00-18:45 PxTP Business Meeting

    Program Committee

    Previous Editions