205 citations · 525 across the 28 of their papers we have counts for
5 papers · 1 filter
Effective Homology of the Pushout of Simplicial Sets
Jónathan Heras
In this paper, an algorithm building the effective homology version of the pushout of the simplicial morphisms and , where and are si…
ACL2(ml): Machine-Learning for ACL2
Jónathan Heras, Ekaterina Komendantskaya
ACL2(ml) is an extension for the Emacs interface of ACL2. This tool uses machine-learning to help the ACL2 user during the proof-development. Namely, ACL2(ml) gives hints to the us…
Defining and computing persistent Z-homology in the general case
Ana Romero, Jónathan Heras, Julio Rubio +1
By general case we mean methods able to process simplicial sets and chain complexes not of finite type. A filtration of the object to be studied is the heart of both subjects persi…
HoTT formalisation in Coq: Dependency Graphs \& ML4PG
Jónathan Heras, Ekaterina Komendantskaya
This note is a response to Bas Spitter's email of 28 February 2014 about ML4PG: "We (Jason actually) are adding dependency graphs to our HoTT library: https://github.com/HoTT/HoTT/…
Proof Pattern Search in Coq/SSReflect
Jónathan Heras, Ekaterina Komendantskaya
ML4PG is an extension of the Proof General interface, allowing the user to invoke machine-learning algorithms and find proof similarities in Coq/SSReect libraries. In this paper, w…