Personoj -- Expressing PVS specifications in Dedukti

Personoj allows to translate specifications from the higher order, automated proof assistant PVS into the universal proof checker Dedukti. Personoj uses Lambdapi, an implementation of Dedukti with meta-variables.

This repository contains

• lambdapi files that define the theory of PVS,
• lisp files that implement a translation from PVS to lambdapi,
• scripts and tools to translate PVS specifications.

Requirements

• lambdapi, revision aae26f2d from https://github.com/gabrielhdt/lambdapi.git
• PVS sources, revision pvs7.1

This repository provides files and tools for reproducible builds and translations.

Installing the encoding

bmake -C encoding install

will install the theory of PVS under the package name personoj.

Exporting PVS to Dedukti

Installation

Copy the content of pvs-load.lisp into .pvs.lisp, replacing PVSDKPATH with the path (absolute or relative to $HOME) to the exporter directory.

Usage

See tools/README.md.