Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs (Q6059221): Difference between revisions

From MaRDI portal
Set OpenAlex properties.
ReferenceBot (talk | contribs)
Changed an Item
 
Property / cites work
 
Property / cites work: Sequent calculi for induction and infinite descent / rank
 
Normal rank
Property / cites work
 
Property / cites work: Untersuchungen über das logische Schliessen. I / rank
 
Normal rank
Property / cites work
 
Property / cites work: Cyclic proofs with ordering constraints / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q3384901 / rank
 
Normal rank
Property / cites work
 
Property / cites work: Mechanically certifying formula-based Noetherian induction reasoning / rank
 
Normal rank
Property / cites work
 
Property / cites work: Q5227521 / rank
 
Normal rank
Property / cites work
 
Property / cites work: The size-change principle for program termination / rank
 
Normal rank
Property / cites work
 
Property / cites work: Büchi Complementation and Size-Change Termination / rank
 
Normal rank
Property / cites work
 
Property / cites work: Descente Infinie + Deduction / rank
 
Normal rank
Property / cites work
 
Property / cites work: Term Rewriting and All That / rank
 
Normal rank
Property / cites work
 
Property / cites work: Certification of Automated Termination Proofs / rank
 
Normal rank
Property / cites work
 
Property / cites work: Isabelle/HOL. A proof assistant for higher-order logic / rank
 
Normal rank

Latest revision as of 10:23, 3 August 2024

scientific article; zbMATH DE number 7759321
Language Label Description Also known as
English
Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
scientific article; zbMATH DE number 7759321

    Statements

    Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs (English)
    0 references
    0 references
    2 November 2023
    0 references
    automated reasoning
    0 references
    cyclic induction
    0 references
    first-order logic with inductive definitions
    0 references
    proof certification
    0 references
    Coq
    0 references
    E-\textsc{Cyclist}
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references