sarsko/CreuSAT

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

Language: Rust - Size: 169 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 637 - Forks: 12

guicho271828/latplan

LatPlan : A domain-independent, image-based classical planner

Language: Python - Size: 3.28 MB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 85 - Forks: 19

stanford-centaur/PyPantograph

A Machine-to-Machine Interaction System for Lean 4.

Language: Python - Size: 46.9 MB - Last synced at: about 1 hour ago - Pushed at: 6 days ago - Stars: 83 - Forks: 18

dex3r/GPT-Codemaster

Automatic programming by creating Pull Requests from Issues using LLMs

Language: C# - Size: 75.2 KB - Last synced at: 14 days ago - Pushed at: about 2 years ago - Stars: 59 - Forks: 4

Tractables/LogicCircuits.jl

Logic Circuits from the Juice library

Language: Julia - Size: 4.55 MB - Last synced at: 1 day ago - Pushed at: 11 months ago - Stars: 48 - Forks: 4

conp-solutions/mergesat Fork of niklasso/minisat

configurable, high-performance SAT solver, implementing incremental solving interface of MiniSat and IPASIR. Based on MiniSat (minisat.se)

Language: C++ - Size: 1.71 MB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 33 - Forks: 3

chasenorman/CanonicalLean

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

Language: C - Size: 6.15 MB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 31 - Forks: 0

contrast-zone/t-rewriter.js

(experimental) Conceptual s-expression based typed term graph rewriting system

Language: JavaScript - Size: 1.34 MB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 29 - Forks: 3

chasenorman/Canonical

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

Language: Lean - Size: 114 KB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 26 - Forks: 1

bio-ontology-research-group/onto2vec

Representation learning for ontologies and their annotations

Language: Groovy - Size: 83 KB - Last synced at: about 1 year ago - Pushed at: about 5 years ago - Stars: 20 - Forks: 3

julianmendez/cel

A lightweight Description Logic reasoner for large-scale biomedical ontologies

Language: Common Lisp - Size: 38 MB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 17 - Forks: 3

nyu-acsys/raven

An automated deductive program verifier based on concurrent separation logic

Language: OCaml - Size: 8.17 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 14 - Forks: 1

julianmendez/jcel

Reasoner for the description logic EL+.

Language: Java - Size: 36.2 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 14 - Forks: 6

CarsonScott/Automated-Logical-Systems

Distributed constraint satisfaction with recursive message-passing agents

Language: Python - Size: 21.5 KB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 14 - Forks: 1

julianmendez/born

Bayesian Ontology Reasoner

Language: Java - Size: 4.27 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 13 - Forks: 6

imandra-ai/cme-mdp

Imandra Modelling Language CME MDP Model

Language: Jupyter Notebook - Size: 2.17 MB - Last synced at: about 1 month ago - Pushed at: about 5 years ago - Stars: 13 - Forks: 3

bio-ontology-research-group/Onto2Graph

Generating graph structures from OWL ontologies

Language: JavaScript - Size: 97.7 MB - Last synced at: about 7 hours ago - Pushed at: over 7 years ago - Stars: 12 - Forks: 1

imandra-ai/ipl-examples

Imandra Protocol Language example models

Size: 117 KB - Last synced at: 2 months ago - Pushed at: 9 months ago - Stars: 11 - Forks: 1

MachSMT/MachSMT

MachSMT: An ML-Driven Algorithm Selection tool for SMT Solvers

Language: Python - Size: 1.47 GB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 10 - Forks: 4

bio-ontology-research-group/AberOWL

Ontology repository that provides Reasoning as as Service

Language: Groovy - Size: 273 MB - Last synced at: about 7 hours ago - Pushed at: 30 days ago - Stars: 9 - Forks: 2

TathagataChakraborti/mmp

Explanations in Multi-Model Planning

Language: Python - Size: 104 KB - Last synced at: about 2 years ago - Pushed at: over 5 years ago - Stars: 9 - Forks: 2

maxadamski/reasonable-embeddings

A novel approach to learning concept embeddings and approximate reasoning in ALC knowledge bases with deep neural networks

Language: Jupyter Notebook - Size: 29 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 8 - Forks: 2

Herb-AI/HerbSWIPL.jl

Julia wrapper around SWI Prolog

Language: Julia - Size: 22.5 KB - Last synced at: about 2 years ago - Pushed at: about 3 years ago - Stars: 8 - Forks: 0

galactose/wviews

Wviews is an artificial intelligence system extension for generating world view answer sets for epistemic logic programs

Language: Python - Size: 114 KB - Last synced at: almost 2 years ago - Pushed at: about 7 years ago - Stars: 8 - Forks: 0

ModelWriter/Tarski

A Platform for Automated Analysis of Traceability (WP3)

Language: Java - Size: 200 MB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 8 - Forks: 1

leoprover/scala-tptp-parser

A parser for the TPTP logic languages for automated theorem proving written in Scala

Language: Scala - Size: 168 KB - Last synced at: 11 days ago - Pushed at: about 2 months ago - Stars: 6 - Forks: 6

yrevar/inverse_rl

Good intention is all you need!

Language: Jupyter Notebook - Size: 80.4 MB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 6 - Forks: 2

seonghobae/kaefa

# kaefa kwangwoon automated exploratory factor analysis for improving research capability to identify unexplained factor structure with complexly cross-classified multilevel structured data in R environment

Language: R - Size: 90.1 MB - Last synced at: 5 days ago - Pushed at: 11 months ago - Stars: 5 - Forks: 0

CryptoSolvers/CryptoSolve

Generate and Verify Cryptographic Modes of Operation using Symbolic Methods

Language: Python - Size: 1.53 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 3 - Forks: 0

symcollab/CryptoSolve 📦

Moved to https://github.com/CryptoSolvers/CryptoSolve

Language: Python - Size: 85.9 MB - Last synced at: 6 days ago - Pushed at: about 2 years ago - Stars: 3 - Forks: 0

mi-ki/cardCryptoVerification

This program introduces formal verification to card-based cryptography by providing a technique which automatically finds new protocols using as few as possible operations and searches for lowest bounds on card-minimal protocols.

Language: C - Size: 43 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 3 - Forks: 1

ModelWriter/AlloyInEcore

Embedding of First-Order Relational Logic into Meta-Object Facility

Language: Java - Size: 135 MB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 3 - Forks: 1

psmoros/AutomatedInference

Open source educational tool for argumentation framework visualisation and semantic inference.

Language: Python - Size: 33.2 KB - Last synced at: about 2 months ago - Pushed at: about 7 years ago - Stars: 3 - Forks: 0

kovzol/ag

Towards an Automated Geometer

Language: HTML - Size: 12 MB - Last synced at: 3 months ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 1

ArthurPrewette/Lecture-Buddy

Automatically generates OCR-enabled PDF's and transcriptions of online lectures.

Language: Python - Size: 32.2 KB - Last synced at: about 2 years ago - Pushed at: about 2 years ago - Stars: 2 - Forks: 1

mi-ki/voting-rule-argumentation

Towards automatic voting rule argumentation by using computer-aided verification such as software bounded model checking.

Language: C - Size: 6.32 MB - Last synced at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 2 - Forks: 1

ivan-ristovic/BDD 📦

Automated Reasoning course project - Binary Decision Diagrams C++ implementation and paper (in Serbian)

Language: TeX - Size: 2.68 MB - Last synced at: about 2 years ago - Pushed at: almost 7 years ago - Stars: 2 - Forks: 0

AbstractionsLab/satrap-dl

SATRAP-DL (Semi-Automated Threat Reconnaissance and Analysis Powered by Description Logics) aims at the development of a platform for interactive computer-aided analysis of cyber threat intelligence driven by logic-based automated reasoning and inference.

Language: Python - Size: 5.01 MB - Last synced at: 25 days ago - Pushed at: 25 days ago - Stars: 1 - Forks: 0

greati/logicantsy

Prototypical library and CLI assistant for research in logic.

Language: C++ - Size: 5.88 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0

NeuralCoder3/prooftrees

Exploration of interactive inference rule application/proofs using a unification approach.

Language: TypeScript - Size: 11.6 MB - Last synced at: about 1 month ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0

srosalino/Intelligent_Systems_Investigations

Series of 11 works, covering: State-Space Representations, Search, Adversarial Search, Logic, Automated Reasoning, Reasoning with Uncertainty and Vagueness and Machine Learning

Language: Jupyter Notebook - Size: 4.31 MB - Last synced at: 3 months ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0

luisalejandrobf/ForwardChainingInference

Implementation of the Forward Chaining Algorithm in C++, a widely used inference engine in the field of artificial intelligence, commonly applied in expert systems for automated reasoning. The repository includes the complete source code and example input files for defining rules and known facts. Instructions are available in English and Spanish.

Language: C++ - Size: 23.4 KB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 1 - Forks: 0

jaalonso/Explorando-con-Lean

Explorando formalizaciones con Lean

Language: Lean - Size: 37.1 KB - Last synced at: about 2 months ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0

aureleeNet/formalizations

This repository collects project-relevant Isabelle/HOL formalizations.

Language: Isabelle - Size: 102 KB - Last synced at: about 2 years ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 0

liamjdavis/Sudoku-SMT-Solvers

Python Package for solving sudoku with SAT and SMT.

Language: Jupyter Notebook - Size: 5.95 MB - Last synced at: about 1 month ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

leoprover/ask

Stand-alone Skolemizer for TPTP formulas

Language: Scala - Size: 567 KB - Last synced at: about 2 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

aabs/inference-engine

A simple inference engine using SPARQL to materialise inferences for RDFS and OWL2

Language: C# - Size: 93.8 KB - Last synced at: about 1 year ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

zucchi99/Project-Automated-Reasoning

Calculation of a possible sharing of a quota between entities with different priorities and many constraints, using SAT-Solver or Answer Set Programming

Language: Python - Size: 1.07 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

jaalonso/Cursos_de_RA

Recopilación de cursos de razonamiento automático.

Size: 15.6 KB - Last synced at: about 2 months ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

chrisjpm/holbert Fork of liamoc/holbert

A graphical interactive proof assistant designed for education. My contributions: applying rules by elimination, proofs by induction, proofs by cases, multi-axiom element and misc css styling. Honours report grade: 76% :tada:

Language: Haskell - Size: 13.3 MB - Last synced at: almost 2 years ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 0

FlorianCassayre/semester-project 📦

Semester Project at LARA (EPFL)

Language: Scala - Size: 301 KB - Last synced at: 8 days ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 1

aztek/phd-thesis

Automated Theorem Proving with Extensions of First-Order Logic

Language: TeX - Size: 2.06 MB - Last synced at: about 2 months ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0

JuanCasado/CONOCIMIENTO_Y_RAZONAMIENTO_AUTOMATIZADO

Automated knowledge and reasoning

Language: Prolog - Size: 6.16 MB - Last synced at: 12 months ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 3

DerJesko/Rusty_Satellite

Language: Rust - Size: 103 KB - Last synced at: almost 2 years ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 0

bio-ontology-research-group/oboconsistencytest

Language: Groovy - Size: 2.48 MB - Last synced at: about 1 year ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 0