cnf

An automatic theorem prover in OCaml for typed higher-order logic with equality, datatypes and arithmetic, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.

prototype experimental ocaml computer-science-algorithms logic polymorphism cnf superposition saturation induction symbolic-computation prover rewriting

Updated Jul 22, 2020
OCaml

ellisonch / CFGLib

Star

Probabilistic Context Free Grammar (PCFG) Library for C#

parser grammar cnf parse-trees context-free-grammar parse-forests earley parsing-algorithm cyk random-grammars

Updated Sep 12, 2018
C#

meelgroup / bosphorus

Star

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter

cnf cryptoanalysis sat dimacs anf anf-simplifications

Updated Jun 2, 2020
C++

omec-project / upf-epc

Star

4G/5G Mobile core user plane

docker kubernetes dpdk cnf dataplane 4g upf 5g spgw userplane bess pfcp

Updated Jul 21, 2020
C++

nikos912000 / chomsky-normal-form

Star

Convert a Context Free Grammar (CFG) to Chomsky Normal Form (CNF)

python cnf chomsky cfg

Updated Jun 4, 2014
Python

vsklad / cgen

Star

CGen is a tool for encoding SHA-1 and SHA-256 hash functions into CNF in DIMACS format, also into ANF polynominal system in PolyBoRi output format.

cryptography hash-functions sha2 sha1 sha256 cnf sat dimacs sha-1 satisfiability cnf-encoding

Updated May 5, 2020
C++

maxtuno / slime-sat-solver

Star

A Free World Class High Performance SAT Solver

cnf sat-solver sat satisfiability cnf-clauses cnf-encoding

Updated Oct 21, 2019
C++

BaseMax / CFG2CNF

Star

Python program to convert a Context Free Grammar to Chomsky Normal Form.

python context-free cnf chomsky cfg context-free-grammar context-free-language context-free-grammars

Updated Jun 30, 2020
Python

brilacasck / java-language-parser

Star

A simple compiler for parsing java codes and get syntax errors with CYK algorithm for context free grammars (CFG)

java parser compiler javafx synthesis cnf cfg context-free-grammar cyk java-language syntax-error light-parser easy-parser

Updated Aug 2, 2018
Java

cipherboy / cmsh

Star

High-level Python interface over @msoos's CryptoMiniSat.

python circuit cnf sat high-level satisfiability cryptominisat5

Updated Mar 31, 2020
Python

glnc / minisat-wasm

Star

Compile MiniSat to WebAssembly using emscripten

solver webassembly wasm emscripten cnf sat-solver minisat sat dimacs

Updated Jan 15, 2020
C++

Average-user / LEC

Star

Transformer of logical expressions to CNF and DNF

haskell logic cnf cnf-encoding

Updated May 1, 2018
Haskell

ValidUSA / mysql-query-audit

Star

A query audit plugin for MySQL.

plugin audit mysql-server cnf jira-inf

Updated Apr 4, 2018
C

maxtuno / problem-solving-book

Star

Problem Solving: A Practical Workbook

csp approximation np-hard np-complete cnf slime sat real-world

Updated Nov 8, 2019
Jupyter Notebook

julianthome / ctrans

Star

Basic constraint transformation library

java cnf boolean-algebra dnf constraint-transformation-library

Updated Mar 27, 2018
Java

jcwleo / DPLL-Algorithm

Star

implementing DPLL Algorithm

artificial-intelligence cnf dpll-algorithm

Updated Nov 4, 2017
Python

glnc / microsat

Star

Simple CDCL SAT solver

solver picosat cnf sat dimacs cdcl microsat

Updated May 14, 2020
C

sakateka / plt

Star

study pda cnf chomsky dfa cfg earley-algorithm context-free-grammar cyk-parser dpda sequence-generation cnf-grammer cyk-algorithm

Updated Jun 29, 2020
Rust

vpozdnyakov / sat_solver_resolution

Star

SAT-solver based on resolution method in 2-CNF using PLY

parsing lex ply cnf sat-solver hse 2-sat resolution-rule

Updated Jan 31, 2020
Python

elishadrion / LightUp

Star

Solving LightUp problems with minisat

cnf sat-solver minisat lightup akari

Updated Jun 3, 2019
C++

glnc / microsat-wasm

Star

Compile microsat to WebAssembly using emscripten

solver webassembly wasm cnf sat-solver sat dimacs microsat

Updated May 26, 2020
C

glnc / spur-wasm

Star

Compile SPUR to WebAssembly using emscripten

solver webassembly wasm emscripten cnf sat-solver sat dimacs spur

Updated Feb 5, 2020
C++

itnef / smtx

Star

My first SMT solver (only QF_UF)

satisfiability-modulo-theories logic-programming cnf learning-by-doing sat-solver smt-solver dpll tseitin-transformation cdcl logical-reasoning congruence-closure backjumping cdcl-t sat-solving qf-uf diy-smt

Updated Jul 8, 2020
Haskell

glnc / spass-wasm

Star

Compile SPASS to WebAssembly using emscripten

solver webassembly wasm emscripten cnf theorem-prover max-planck-institute spass

Updated Feb 5, 2020
C

sharsha09 / Inference-Engine

Star

When a query is asked, various sentences from Knowledge Base are inferred and outputs whether the given query can be inferred or not based on the Resolution Algorithm

python knowledgebase cnf lexical-parser