horn

master branch1 version
  • master branchlatestFeb 8, 2026

github.com/giannos-ch/horn

No description declared in shard.yml.

0 stars
0 dependents
License: MIT

Installation

# Add this to your shard.yml
dependencies:
  horn:
    github: giannos-ch/horn
    branch: master

master is a branch, not a release, so this tracks it rather than pinning a version.

Then run:

shards install

shard.yml

Crystal
>= 1.13.2
License
MIT
Author
Giannos Chatziagapis
Target
  • horn from src/horn.cr

Dependencies

This version declares no dependencies.

README

HORN

Higher-Order Reasoning with Negation

Installation

  1. Install Crystal and Shards. See here.
  2. Install tree-sitter:
    • On ubuntu: apt install libtree-sitter-dev
    • On macOS: brew install tree-sitter
  3. Run make.

Usage

$ cat spec/fixtures/program.horn
a,b :: i. p :: i->o. r :: o.
p(a).
r :- ]X:i ~(p X).

?- r.
$ ./bin/horn -f spec/fixtures/program.horn
r =>
T
$ cat spec/fixtures/equals.horn
a,b :: i.
p :: i->o.
p a.

subset, equals :: (i->o)->(i->o)->o.
subset P Q :- ~]X:i P X /\ ~Q X.
equals P Q :- subset P Q, subset Q P.

?- equals p Q_.
$ ./bin/horn -s dnf -f spec/fixtures/equals.horn
((equals p) Q_) =>
(Q_ a), ¬(Q_ b)

Contributors

Documentation

Read the API docs

Built from the current release. The first visit to a release nobody has asked for starts its build.

Links

This branch

Branch
master
Seen
Feb 8, 2026
Crystal
>= 1.13.2
Indexed
yes

Dependents

No indexed shard depends on this one yet.

Repository

github.com/giannos-ch/horn

Metadata

Created
Aug 12, 2026
Updated
Aug 17, 2026
Synced
Aug 17, 2026
Versions
1