The following pages link to Francisco Jesús Martín-Mateos (Q438547):
Displaying 26 items.
- Proof pearl: a formal proof of Higman's lemma in ACL2 (Q438550) (← links)
- (Q877822) (redirect page) (← links)
- Formal correctness of a quadratic unification algorithm (Q877825) (← links)
- Formal proofs about rewriting using ACL2 (Q1610218) (← links)
- (Q1687753) (redirect page) (← links)
- Using abstract stobjs in ACL2 to compute matrix normal forms (Q1687754) (← links)
- Formalization of a normalization theorem in simplicial topology (Q1926582) (← links)
- Modelling algebraic structures and morphisms in ACL2 (Q2349534) (← links)
- Formally verified tableau-based reasoners for a description logic (Q2351147) (← links)
- Formal verification of a generic framework to synthesize SAT-provers (Q2583288) (← links)
- Certified symbolic manipulation (Q2963240) (← links)
- (Q3021901) (← links)
- (Q3062057) (← links)
- Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers (Q3079919) (← links)
- Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials (Q3088007) (← links)
- (Q3408130) (← links)
- A Formally Verified Prover for the $\mathcal{ALC\,}$ Description Logic (Q3523171) (← links)
- ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System (Q3637272) (← links)
- (Q4433996) (← links)
- (Q4437091) (← links)
- (Q4471942) (← links)
- (Q4664924) (← links)
- Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm (Q5172125) (← links)
- Computer Aided Systems Theory – EUROCAST 2005 (Q5394447) (← links)
- Theorem Proving in Higher Order Logics (Q5477667) (← links)
- Logic Based Program Synthesis and Transformation (Q5713948) (← links)
