Presentation

Pangoline is a theorem prover for higher-order logic. It is based on an encoding of polymorphic higher-order logic theories into polymorphic first-order logic theories.

Authors

Pangoline is being developed by Johannes Kanig and Yann Régis-Gianas.

Releases

• Version 0.1 code "Spring": Download - Manual. (This specific version of Ulex is needed.)

Mailing list

• pangoline-dev To discuss about pangoline development.
• pangoline-tickets All tickets/patches notifications go here (read-only / no archives).