Jacob M. Howe

OVERLAY Workshop 2025 Workshop Paper

Extracting Weighted Finite Automata from RNNs via iterative partitioning and spectral learning

• Sandamali Yashodhara Wickramasinghe
• Jacob M. Howe
• Laure Daviaud

NeSy Conference 2019 Conference Paper

Efficient Predicate Invention using Shared NeMuS

• Edjard Mota
• Jacob M. Howe
• Ana Schramm
• Artur S. d'Avila Garcez

Amao is a cognitive agent framework that tackles the invention of predicates with a different strategy as compared to recent advances in Inductive Logic Programming (ILP) approaches like Meta- Intepretive Learning (MIL) technique. It uses a Neural Multi-Space (NeMuS) graph structure to anti-unify atoms from the Herbrand base, which passes in the inductive momentum check. Inductive Clause Learning (ICL), as it is called, is extended here by using the weights of logical components, already present in NeMuS, to support inductive learning by expanding clause candidates with anti-unified atoms. An efficient invention mechanism is achieved, including the learning of recursive hypotheses, while restricting the shape of the hypothesis by adding bias definitions or idiosyncrasies of the language.

TCS Journal 2019 Journal Article

Incremental Closure for Systems of Two Variables Per Inequality

• Jacob M. Howe
• Andy King
• Axel Simon

Subclasses of linear inequalities where each inequality has at most two variables are popular in abstract interpretation and model checking, because they strike a balance between what can be described and what can be efficiently computed. This paper focuses on the TVPI class of inequalities, for which each coefficient of each two variable inequality is unrestricted. An implied TVPI inequality can be generated from a pair of TVPI inequalities by eliminating a given common variable (echoing resolution on clauses). This operation, called result, can be applied to derive TVPI inequalities which are entailed (implied) by a given TVPI system. The key operation on TVPI is calculating closure: satisfiability can be observed from a closed system and a closed system also simplifies the calculation of other operations. A closed system can be derived by repeatedly applying the result operator. The process of adding a single TVPI inequality to an already closed input TVPI system and then finding the closure of this augmented system is called incremental closure. This too can be calculated by the repeated application of the result operator. This paper studies the calculus defined by result, the structure of result derivations, and how derivations can be combined and controlled. A series of lemmata on derivations are presented that, collectively, provide a pathway for synthesising an algorithm for incremental closure. The complexity of the incremental closure algorithm is analysed and found to be O ( ( n 2 + m 2 ) lg ⁡ ( m ) ), where n is the number of variables and m the number of inequalities of the input TVPI system.

NeSy Conference 2017 Conference Paper

Category-based Inductive Learning in Shared NeMuS

• Ana Schramm
• Edjard Mota
• Jacob M. Howe
• Artur S. d'Avila Garcez

NeSy Conference 2017 Conference Paper

Inductive Learning in Shared Neural Multi-Spaces

• Edjard Mota
• Jacob M. Howe
• Artur S. d'Avila Garcez

The learning of rules from examples is of continuing interest to machine learning since it allows generalization from fewer training examples. Inductive Logic Programming (ILP) generates hypothetical rules (clauses) from a knowledge base augmented with (positive and negative) examples. A successful hypothesis entails all positive examples and does not entail any negative example. The Shared Neural Multi-Space (Shared NeMuS) structure encodes first order expressions in a graph suitable for ILP-style learning. This paper explores the NeMuS structure and its relationship with the Herbrand Base of a knowledge-base to generate hypotheses inductively. It is demonstrated that inductive learning driven by the knowledge-base structure can be implementated successfully in the Amao cognitive agent framework, including the learning of recursive hypotheses.

NeSy Conference 2017 Conference Paper

Learning about Actions and Events in Shared NeMuS

• Milena Rodrigues Tenorio
• Edjard Mota
• Jacob M. Howe
• Artur S. d'Avila Garcez

TCS Journal 2012 Journal Article

A pearl on SAT and SMT solving in Prolog

• Jacob M. Howe
• Andy King

A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solver is surprisingly powerful and its elegant use of Prolog constructs is presented as a programming pearl. Furthermore, the SAT solver can be integrated into an SMT framework which exploits the constraint solvers that are available in many Prolog systems.

LOPSTR Conference 2002 Conference Paper

Two Variables per Linear Inequality as an Abstract Domain

• Axel Simon
• Andy King
• Jacob M. Howe

Abstract This paper explores the spatial domain of sets of inequalities where each inequality contains at most two variables — a domain that is richer than intervals and more tractable than general polyhedra. We present a complete suite of efficient domain operations for linear systems with two variables per inequality with unrestricted coefficients. We exploit a tactic in which a system of inequalities with at most two variables per inequality is decomposed into a series of projections — one for each two dimensional plane. The decomposition enables all domain operations required for abstract interpretation to be expressed in terms of the two dimensional case. The resulting operations are efficient and include a novel planar convex hull algorithm. Empirical evidence suggests that widening can be applied effectively, ensuring tractability.

LOPSTR Conference 2000 Conference Paper

Specialising Fininte Domain Programs Using Polyhedra

• Jacob M. Howe
• Andy King

Abstract A procedure is described for tightening domain constraints of finite domain logic programs by applying a static analysis based on convex polyhedra. Individual finite domain constraints are over-approximated by polyhedra to describe the solution space over n integer variables as an n dimensional polyhedron. This polyhedron is then approximated, using projection, as an n dimensional bounding box that can be used to specialise and improve the domain constraints. The analysis can be implemented straightforwardly and an empirical evaluation of the specialisation technique is given.