Haniel Ulises

Classical planning assumes that the agent knows which propositions hold; epistemic planning drops this assumption. The search space consists of pointed Kripke models, each of which must be updated, minimised and compared in full at every node, and goals may be irreducibly modal, for instance that an agent knows the door is open. Performance therefore reduces to three questions: how a Kripke model is represented, how modal formulas are evaluated over it, and how two models are recognised as the same epistemic situation.

Three decisions determine the design. A model is stored as three flat arrays of 64-bit words, for valuation, accessibility and designation, so that modal operators are word-parallel set operations. Formulas are evaluated as extensions: for each subformula the set of worlds where it holds is computed bottom-up and memoised on hash-consed formula identity, which reduces common knowledge to a single greatest fixpoint. Bisimulation contraction assigns world indices in an order determined by the model's structure alone, so bisimilar states serialise identically and duplicate detection is a comparison of 128-bit fingerprints.

Validated against the IεPC 2026 benchmarks, Tracks Basic and Intermediate. Built at UNAM-FI and IPN-ESCOM.

github.com/HanielUlises/Aletheia

The execution layer for epistemic planning on physical robots. It extends PlanSys2 with S5 and KD45 world models, EPDDL domain support and heuristic search over epistemic states, so that multi-robot coordination under partial observability is expressed directly in the planner's formalism.

This sits alongside ALETHEIA, which is the planner proper, and Epistemic-Robotics, which connects both to physical robots under ROS 2. The motivating case is small and concrete. Two robots must retrieve an object from a corridor that may be blocked; a classical planner routes the second robot through it because it treats the world as globally known, and the robot fails on arrival. Here the initial epistemic state represents that uncertainty as two designated worlds, and no route is assigned until the first robot senses the corridor and collapses the belief state.

github.com/HanielUlises/eplansys

An autonomous robot in a partially observable environment must plan with an explicit account of what it does not know. This framework grounds multi-agent task planning in dynamic epistemic logic, so that ignorance is part of the represented state. Each agent maintains a Kripke model of the world; actions are epistemic events that refine the model by product update; and navigation routes are winning regions of μ-calculus reachability formulas computed over the occupancy graph.

The framework distinguishes two goals: that an agent reaches a zone, and that it knows it has reached it; the planner treats them separately. Several projects on this page derive from it. ALETHEIA is the planner, ePlanSys the execution layer, and the collaborative SLAM of the degree thesis the perceptual substrate; this repository connects them to physical robots.

hanielulises.github.io/Epistemic-Robotics
github.com/HanielUlises/Epistemic-Robotics

A fleet of unmanned ground vehicles explores an unknown planar environment, each agent running an independent pose-graph SLAM front end over its own laser observations. Inter-agent connectivity is intermittent, so the fleet-level map is defined as the union of the observations actually delivered, and the implementation models each link explicitly.

Individual occupancy estimates are fused by an operator that is idempotent and order-independent over a bounded join-semilattice, so the same observations arriving in any order give the same map, and delivery is gated by a per-agent link process, so a lost link freezes an agent's contribution without erasing it. The divergence between what an agent knows and what the fleet knows is then measured directly. That divergence is precisely the asymmetry the dynamic epistemic logic layer is meant to reason about, which is what connects this to the planning work.

A second iteration carries the same substrate, unchanged, onto the floor plan of a real building with three agents.

github.com/HanielUlises/ROS-Mobile · Planning/MultiRobot_ws

Every heuristic in current use, whether delete relaxation, landmarks or abstractions, is a human artefact that encodes one structural insight and is fixed once published. Here an outer loop proposes heuristics as linear combinations of named state features, measures the search effort each induces on a benchmark, and uses that measurement to propose better ones. The hypothesis class is restricted to interpretable weight vectors, so that a discovered heuristic can be read, compared with known heuristics and analysed.

The first phase establishes that the loop closes. On Blocksworld under greedy best-first search, weights found after 25 planner invocations reduced node expansions by three quarters on the training instances and by more on held-out ones, with full coverage and no increase in plan cost. The result is limited to one domain, one optimiser seed and one objective. Later work adds admissible components, landmarks and pattern databases combined by saturated cost partitioning, as the basis for comparing evolutionary, reinforcement-learning and program-synthesis methods under a common objective and search engine.

github.com/HanielUlises/Heuristic-Discovery

A research implementation for studying fixed-point and modal logics as specifications for motion planning. The present phase establishes the logical core, namely finite Kripke structures, an explicit abstract syntax for the modal μ-calculus, well-formedness and fragment validation, and model checking over finite models by explicit Tarski and Knaster fixed-point iteration.

The formalism reproduced is that of Larocque and Liu, who adapt the deterministic fragment and its model-checking procedure from Karaman and Frazzoli. This phase introduces no new theory. Its purpose is a mathematically faithful, independently verified core on which the later phases depend; the planner is deferred to those phases.

github.com/HanielUlises/MuMotion

Model checking a branching-time logic is a fixpoint computation over the powerset lattice, which is complete and of finite height; by the Knaster–Tarski theorem the modal operators reach their least and greatest fixpoints by Kleene iteration in at most |S| steps. Every CTL operator is then a sequence of existential pre-image applications interleaved with set operations, and the existential pre-image is a sparse matrix-vector product over the boolean semiring with the transposed transition relation. The implementation rests on this observation, since sparse matrix-vector products map efficiently onto GPU hardware.

The transition relation resides on the device in compressed sparse row form, state sets are bitmaps assembled by warp ballot without atomics, and model products are constructed entirely on the GPU. Fair cycles require strongly connected components, which are found by parallel colouring. Structural invariants are verified at construction: totality of the relation is checked and successor lists are sorted, which makes the CSR layout a function of the model alone, independent of the order in which transitions are supplied.

Every device computation has a sequential counterpart verified step by step against it.

github.com/HanielUlises/KripCUDA

Whether two finite structures satisfy the same first-order sentences with at most k variables and quantifier rank at most q is decided by an exhaustive game between Spoiler and Duplicator. The question is how much of that decision a neural sequence model can acquire from labelled examples, and whether what it acquires carries over to larger structures, to deeper distinctions, and to families built to defeat combinatorial heuristics.

The labels are exact. A C++ solver computes the separating rank by a jointly named refinement of the types of partial pebble configurations, in time O(q k (n+1)^k log n), which makes k = 3, q = 4 and n = 50 a matter of milliseconds. The same tables are a complete winning strategy for Spoiler, from which a distinguishing sentence of exactly that rank is read off, and every sentence is certified by a checker whose soundness is proved in Lean 4. All 17,040 sentences of the dataset were accepted.

The learner is an axial tuple transformer over the tensor of atomic types of k-tuples, in which attention along axis i corresponds to a move of pebble i. Its separating power lies between two logics: it cannot separate C^k-equivalent structures, and with L layers it decides equivalence exactly up to rank L + 1 on bounded universes. Each test split varies a single condition (size; family, with CFI and strongly regular graphs absent from training; and rank), so each failure can be attributed to one cause.

github.com/HanielUlises/elementary-transformer

A formalisation of possible-world and situation semantics in the higher-order modal and situation-theoretic tradition of Zalta, Fine, and Barwise and Perry. Every theorem is checked by the Lean kernel, and every remaining gap is tabulated as an explicit open proof obligation, so the extent of the formalisation is stated precisely.

The development is layered. An ontological grounding core fixes the primitives and their algebra, covering encoding, situations, truth, parthood, dependence and abstract objects. A modality layer postulates the S5 calculus over frames and operators. A situation layer builds worlds and their meet-semilattice on top, with extensionality and infima proved as theorems. It is the formal counterpart of the philosophical work.

github.com/HanielUlises/Possible-World-Semantics

An embedded language for propositional logic with its own syntax, substitution, evaluation semantics and pretty-printing, and on top of it conversion to normal forms, a clause representation, resolution and a DPLL procedure. Because these are defined inside a proof assistant, the definitions are the same objects against which later statements about them are proved.

It provides the propositional base. The planned extensions are modal and epistemic logic and algebraic simplification, which connect it to the Kripke-model work elsewhere on this page.

github.com/HanielUlises/lean-logic-dsl

A decision procedure for propositional satisfiability built as complete DPLL, with unit propagation, pure literal elimination and backtracking search over the assignment tree. It classifies a formula as a tautology, a contingency or a contradiction, by a procedure whose completeness follows from the structure of the search.

The extension in progress lifts this to DPLL(T), where the propositional search is coupled to a theory solver and the boolean skeleton is checked for consistency against the theory at each step. Work in progress, and marked as such.

github.com/HanielUlises/Theorem-Prover

Robot kinematics is a system of polynomial equations over a finite-dimensional quotient ring, and varietas solves it as such by elimination theory. The tangent half-angle substitution rationalises the forward kinematics map, a Gröbner basis of the resulting ideal is computed offline, and the inverse kinematics is resolved at runtime by eigendecomposition of a fixed-size action matrix.

Completeness is certified. By the Finiteness Theorem the quotient algebra is finite dimensional exactly when the variety is finite, a condition decidable from the leading terms of the basis alone, and its dimension bounds the number of solutions counted with multiplicity. IKFast pattern-matches known kinematic structures and fails silently outside them; varietas either returns a solution set with this guarantee or identifies the hypothesis of the Extension Theorem that was violated.

Exactness is enforced at the point where geometry enters the computation. Buchberger's algorithm discards a critical pair when the S-polynomial reduces to zero, a structural test on an empty term list; in floating point, cancellation leaves a residue, the pair survives, and the finiteness verdict read off the leading monomials then describes a different ideal. The offline stage therefore runs over ℚ with GMP-backed rationals. The URDF front end follows the same principle and recovers exact geometry over the rationals by projective approximation of quaternions, since a URDF encodes π/2 as the literal 1.57079632679, whose exact rational reading describes a slightly different mechanism. Validated against KDL on a KUKA iiwa.

github.com/HanielUlises/varietas

A surface is given by a formula and rendered in three dimensions together with its Gaussian curvature and its geodesics. The name refers to Gauss's Theorema Egregium: the curvature is an intrinsic invariant of the surface, determined by its metric alone and independent of any embedding in ℝ³. Surfaces are specified in four forms: explicit, parametric, implicit (rendered by raymarching), and by first fundamental form with an optional embedding for display.

Every formula is parsed and differentiated symbolically, so the derived quantities are exact to floating-point precision. This is essential for curvature: a finite-difference estimate on a coarse mesh produces plausible images with quantitatively incorrect values, and the visualiser is designed so that the rendered image and the computed value agree.

github.com/HanielUlises/egregium

A template library that treats geometric primitives and graph abstractions as a single subject. Types expose their topological properties through the interface and algorithms state formal contracts on their inputs, so the separation between topology and representation is enforced by the compiler.

The library supports the three constant-curvature geometries simultaneously. Incidence and distance predicates are therefore written with the curvature as an explicit parameter, a stronger design constraint than the Euclidean case alone imposes.

github.com/HanielUlises/PolyGraph

Three complementary approaches to the same equations. Classical numerical schemes cover finite differences, finite elements and finite volumes. Physics-informed neural networks embed the PDE residual, together with the initial and boundary conditions, directly in the loss, so the constraint is enforced through the objective function.

The inverse formulation uses the network to infer unknown coefficients, parameters or source terms of the equation from observed data. The solver thereby becomes an identification method, and the comparison with classical schemes becomes a comparison of the prior knowledge each approach assumes.

github.com/HanielUlises/Computational-PDEs

Lane segmenters are usually evaluated by mask overlap with the annotation. A model predictive controller consumes the vehicle's lateral offset within the lane and the curvature of the road ahead, so these are the quantities measured here. Overlap averaged over the natural frame distribution is insensitive to tight curves, which are precisely the frames that matter for control.

Training uses a curvature-stratified subset of CurveLanes with a curvature-sensitive cost, which flattens the distribution and raises performance on the tails. The detection gap between straight road and tight curves decreased from 21.6 to 3.9 points. Calibration is a pinhole model fitted by lane parallelism and validated independently against the vanishing point, so the validation does not depend on the fitting assumption.

The full chain was ported to C++: preprocessing, the network through ONNX Runtime on a half-precision TensorRT engine, and all of the geometry. The port is verified against the Python reference with golden vectors. It generalises to KITTI without retraining, recovering the lane in 94.7% of frames.

Play segmentation demo

Play KITTI demo

github.com/HanielUlises/curvature-aware-lane-seg

GrabCut requires a human to mark the initial trimap, which excludes it from automated pipelines. Here the trimap is predicted by a graph convolutional network over superpixels, seeded by a training-free saliency prior computed from the image itself, so the method requires no annotated initialisation at inference time.

Mean IoU on DUTS is 0.584 against 0.109 for the trivial prediction, with 187,826 parameters.

github.com/HanielUlises/GCN-GrabCut

A layered collection of image processing and computer vision work. Part of it is didactic, implementing core techniques so that each algorithm is legible in the code, with correctness and readability prioritised over premature optimisation. The remainder is project work, some consolidating established methods and some developed from open conceptual questions.

Background subtraction, filtering, feature detection, stereo, and tracking all appear here, drawing on Szeliski and on the standard literature. The wider intent is to use the repository as a place to think critically about the structure of visual algorithms while extending toward scientific computing in modern C++.

github.com/HanielUlises/High-Performance-CV

Modular implementations of classical machine learning algorithms covering supervised and unsupervised learning, model validation, clustering, dimensionality reduction, and the supporting mathematical utilities. Each module operates independently and exposes a concise interface.

The codebase follows a minimal-dependency design, resting on the standard library and a set of self-contained headers, which gives predictable performance and full control over memory. The formulations are mathematically explicit, so the statistical assumptions and convergence parameters of each algorithm are visible in its interface.

github.com/HanielUlises/machine-learning-cpp

Robots are declared once, in a registry, and a single launch entry point resolves it and dispatches to the requested robot, variant and backend: RViz, Gazebo, Gazebo under ros2_control, or mock hardware with no simulator. An unrecognised value is rejected at launch, with the alternatives the registry offers.

For the G1, in its 23 and 29 degree-of-freedom builds, a C++ library reads the URDF itself and exposes a canonical joint order, limits with clamping, forward kinematics for any link, the whole-body centre of mass and gravity torques. It has no runtime ROS dependency, so offline tooling links against it directly, and its tests run against the description files, so they fail if the robot changes shape. The ros2_control controller is built on that model.

Play demo

github.com/HanielUlises/ROS-Humanoids

Peripheral definitions are written from the reference manual, independently of the vendor HAL, and cover RCC and GPIO. UART2 transmission is brought up by configuring the alternate function, computing the baud rate register by hand and polling the status register. A SysTick time base and standard output redirected over the serial port complete the minimum required to work without a debugger attached.

Every layer between the code and the silicon is written and verified explicitly.

github.com/HanielUlises/Embedded