Small, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting
| Autor: | Färber, Michael |
|---|---|
| Přispěvatelé: | Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: | |
| Popis: | Several proof assistants, such as Isabelle or Coq, can concurrently check multiple proofs. In contrast, the vast majority of today's small proof checkers either does not support concurrency at all or only limited forms thereof, restricting the efficiency of proof checking on multi-core processors. This work presents a small proof checker with support for concurrent proof checking, achieving state-of-the-art performance in both concurrent and nonconcurrent settings. The proof checker implements the lambda-Pi calculus modulo rewriting, which is an established framework to uniformly express a multitude of logical systems. The proof checker is faster than the reference proof checker for this calculus, Dedukti, on all of five evaluated datasets obtained from proof assistants and interactive theorem provers. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|