205 citations · 525 across the 28 of their papers we have counts for
7 papers · 1 filter
Exploiting Parallelism in Coalgebraic Logic Programming
Ekaterina Komendantskaya, Martin Schmidt, Jónathan Heras
We present a parallel implementation of Coalgebraic Logic Programming (CoALP) in the programming language Go. CoALP was initially introduced to reflect coalgebraic semantics of log…
Proof-Pattern Recognition and Lemma Discovery in ACL2
Jónathan Heras, Ekaterina Komendantskaya, Moa Johansson +1
We present a novel technique for combining statistical machine learning for proof-pattern recognition with symbolic methods for lemma discovery. The resulting tool, ACL2(ml), gathe…
A certified reduction strategy for homological image processing
María Poza, César Domínguez, Jónathan Heras +1
The analysis of digital images using homological procedures is an outstanding topic in the area of Computational Algebraic Topology. In this paper, we describe a certified reductio…
Statistical Proof Pattern Recognition: Automated or Interactive?
Jónathan Heras, Ekaterina Komendantskaya
In this paper, we compare different existing approaches employed in data mining of big proof libraries in automated and interactive theorem proving.
Verifying a platform for digital imaging: a multi-tool strategy
Jónathan Heras, Gadea Mata, Ana Romero +2
Fiji is a Java platform widely used by biologists and other experimental scientists to process digital images. In particular, in our research - made together with a biologists team…
ML4PG in Computer Algebra verification
Jónathan Heras, Ekaterina Komendantskaya
ML4PG is a machine-learning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof pattern…