English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We investigate here a new version of the Calculus of Inductive Constructions(CIC) on which the proof assistant Coq is based: the Calculus of CongruentInductive Constructions, which truly extends CIC by building in arbitraryfirst-order decision procedures: deduction is still in charge of the CICkernel, while computation is outsourced to dedicated first-order decisionprocedures that can be taken from the shelves provided they deliver a proofcertificate. The soundness of the whole system becomes an incremental propertyfollowing from the soundness of the certificate checkers and that of thekernel. A detailed example shows that the resulting style of proofs becomescloser to that of the working mathematician.

From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures