QR Code

Checking Zenon Modulo Proofs in Dedukti

Dedukti has been proposed as a universal proof checker. It is a logical framework based on the lambda Pi calculus modulo that is used as a backend to verify proofs coming from theorem provers, especially those implementing some form of rewriting. We present a shallow embedding into Dedukti of proofs...

Whakaahuatanga katoa

I tiakina i:
Ngā taipitopito rārangi puna kōrero
Ngā kaituhi matua: Raphaël Cauderlier, Pierre Halmagrand
Hōputu: Artigo
Reo:Inglês
I whakaputaina: Open Publishing Association 2015-07-01
Rangatū:Electronic Proceedings in Theoretical Computer Science
Urunga tuihono:http://arxiv.org/pdf/1507.08719v1
Ngā Tūtohu: Tāpirihia he Tūtohu
Kāore He Tūtohu, Me noho koe te mea tuatahi ki te tūtohu i tēnei pūkete!