![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
4th PxTP@CADE 2015: Berlin, Germany
- Cezary Kaliszyk
, Andrei Paskevich:
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015. EPTCS 186, 2015 - Giselle Reis:
Importing SMT and Connection proofs as expansion trees. 3-10 - Quentin Heath, Dale Miller
:
A framework for proof certificates in finite state exploration. 11-26 - Christoph Benzmüller
, Maximilian Claus, Nik Sultana:
Systematic Verification of the Modal Logic Cube in Isabelle/HOL. 27-41 - Mark Adams:
The Common HOL Platform. 42-56 - Raphaël Cauderlier, Pierre Halmagrand:
Checking Zenon Modulo Proofs in Dedukti. 57-73 - Ali Assaf, Guillaume Burel:
Translating HOL to Dedukti. 74-88 - Ali Assaf, Raphaël Cauderlier:
Mixing HOL and Coq in Dedukti (Extended Abstract). 89-96
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.