A Rocq formalization defines simplicial Lagrange finite elements as records with geometric data, polynomial approximations, and unisolvence proofs for any dimension and polynomial degree.
Automatically Proving and Dispr oving Feasibility Conditions
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
fields
cs.LO 4verdicts
UNVERDICTED 4roles
background 1polarities
background 1representative citing papers
The Confluence Framework provides a modular strategy to automatically prove and disprove confluence for a broad class of generalized term rewriting systems.
Develops syntax and semantics for polymorphic DHOL, extends its translation to HOL, and implements the result in a logic-embedding tool for evaluation on TPTP problems.
Introduces Abduction Prover that constructs proof scripts in Isabelle/HOL by identifying useful conjectures via abductive reasoning.
citing papers explorer
-
A Rocq Formalization of Simplicial Lagrange Finite Elements
A Rocq formalization defines simplicial Lagrange finite elements as records with geometric data, polynomial approximations, and unisolvence proofs for any dimension and polynomial degree.
-
Proving Confluence in the Confluence Framework with CONFident
The Confluence Framework provides a modular strategy to automatically prove and disprove confluence for a broad class of generalized term rewriting systems.
-
Polymorphism Meets DHOL
Develops syntax and semantics for polymorphic DHOL, extends its translation to HOL, and implements the result in a logic-embedding tool for evaluation on TPTP problems.
-
Abduction Prover in Isabelle/HOL
Introduces Abduction Prover that constructs proof scripts in Isabelle/HOL by identifying useful conjectures via abductive reasoning.