LinearOneLinearOne is a prototype theorem prover for first-order (multiplicative, intuitionistic) linear logic.
Stars: ✭ 16 (-69.23%)
Mutual labels: theorem-proving, first-order-logic
pyproverResolution theorem proving for predicate logic in pure Python.
Stars: ✭ 71 (+36.54%)
Mutual labels: theorem-proving, first-order-logic
LeanHomepage
Theorem Proving in Lean
FAQ
Stars: ✭ 2,006 (+3757.69%)
Mutual labels: theorem-proving
informatica-publicPublic code developed during my MSc study at University of Bologna
Stars: ✭ 79 (+51.92%)
Mutual labels: theorem-proving
ostrichAn SMT Solver for string constraints
Stars: ✭ 18 (-65.38%)
Mutual labels: theorem-proving
rusty-razorRazor is a tool for constructing finite models for first-order theories
Stars: ✭ 54 (+3.85%)
Mutual labels: theorem-proving
fm-notesUnassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Stars: ✭ 19 (-63.46%)
Mutual labels: theorem-proving
Set-TheoryCoq encoding of ZFC and formalization of the textbook Elements of Set Theory
Stars: ✭ 55 (+5.77%)
Mutual labels: theorem-proving
archsatA proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.
Stars: ✭ 20 (-61.54%)
Mutual labels: theorem-proving
Leo-IIIAn Automated Theorem Prover for Classical Higher-Order Logic with Henkin Semantics
Stars: ✭ 29 (-44.23%)
Mutual labels: theorem-proving
lsw2OWL and Semantic Web toolkit for Common Lisp, used for construction and reasoning over ontologies and ontology-structured data
Stars: ✭ 22 (-57.69%)
Mutual labels: first-order-logic
awesome-rust-formalized-reasoningAn exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Stars: ✭ 185 (+255.77%)
Mutual labels: theorem-proving
gaptGAPT: General Architecture for Proof Theory
Stars: ✭ 83 (+59.62%)
Mutual labels: theorem-proving
FstarA Proof-oriented Programming Language
Stars: ✭ 2,171 (+4075%)
Mutual labels: theorem-proving
coq jupyterJupyter kernel for Coq
Stars: ✭ 70 (+34.62%)
Mutual labels: theorem-proving
CoqCoq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Stars: ✭ 3,566 (+6757.69%)
Mutual labels: theorem-proving
pomagmaAn inference engine for extensional untyped λ-calculus
Stars: ✭ 15 (-71.15%)
Mutual labels: theorem-proving
consistencyImplementation of models in our EMNLP 2019 paper: A Logic-Driven Framework for Consistency of Neural Models
Stars: ✭ 26 (-50%)
Mutual labels: first-order-logic
tarskiTarski - An AI Planning Modeling Framework
Stars: ✭ 30 (-42.31%)
Mutual labels: first-order-logic
TheoLogVorlesungsunterlagen "Theoretische Informatik und Logik", Fakultät Informatik, TU Dresden
Stars: ✭ 20 (-61.54%)
Mutual labels: first-order-logic
