GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → gallais → agda-presburger

gallais / agda-presburger

Licence: other
Deciding Presburger arithmetic in agda

Programming Languages

Agda
84 projects

Labels

agdaformalizationdecision-procedurepresburger-arithmetic

Projects that are alternatives of or similar to agda-presburger

agda
The theory of algebraic graphs formalised in Agda
Stars: ✭ 67 (+157.69%)
Mutual labels:  agda
SymmetryBookFormalization
Univalent mathematics in Agda
Stars: ✭ 117 (+350%)
Mutual labels:  agda
agda-mode
Accessing Agda's interaction mode via command line & external tactic for Agda.
Stars: ✭ 26 (+0%)
Mutual labels:  agda
Agda
Agda is a dependently typed programming language / interactive theorem prover.
Stars: ✭ 1,699 (+6434.62%)
Mutual labels:  agda
agda-fragment
Algebraic proof discovery in Agda
Stars: ✭ 28 (+7.69%)
Mutual labels:  agda
universe-of-syntax
A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.
Stars: ✭ 16 (-38.46%)
Mutual labels:  agda
gentle-intro-to-reflection
A slow-paced introduction to reflection in Agda. ---Tactics!
Stars: ✭ 58 (+123.08%)
Mutual labels:  agda
tt-in-cubical
Type Theory in Type Theory using Cubical Agda
Stars: ✭ 12 (-53.85%)
Mutual labels:  agda
cubical-categories
Category theory formalized in cubical agda
Stars: ✭ 20 (-23.08%)
Mutual labels:  agda
cat
A formalization of category theory in cubical Agda
Stars: ✭ 50 (+92.31%)
Mutual labels:  agda
language-agda
Agda language support for the Atom editor
Stars: ✭ 13 (-50%)
Mutual labels:  agda
agda-language-server
Language Server for Agda
Stars: ✭ 81 (+211.54%)
Mutual labels:  agda
frp agda
Functional Reactive Programming with Agda
Stars: ✭ 22 (-15.38%)
Mutual labels:  agda
agda-from-nothing
A workshop on learning Agda with minimal prerequisites.
Stars: ✭ 74 (+184.62%)
Mutual labels:  agda
system-F
Formalization of the polymorphic lambda calculus and its parametricity theorem
Stars: ✭ 20 (-23.08%)
Mutual labels:  formalization
cubical-1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
Stars: ✭ 93 (+257.69%)
Mutual labels:  agda
blt
Lattice-based integer linear programming solver
Stars: ✭ 60 (+130.77%)
Mutual labels:  decision-procedure
AutoInAgda
Proof automation – for Agda, in Agda.
Stars: ✭ 38 (+46.15%)
Mutual labels:  agda
ataca
A TACtic library for Agda
Stars: ✭ 47 (+80.77%)
Mutual labels:  agda
TypeTopology
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
Stars: ✭ 132 (+407.69%)
Mutual labels:  agda
View All Similar Projects ➔

Deciding Presburger arithmetic in agda.

This repository contains a cleaned up version of the work done in Nottingham under Thorsten Altenkirch's supervision.

It is based on Amine Chaieb and Tobias Nipkow's formalization of a similar procedure in HOL.

Dependencies

This development has been typechecked with:

  • Agda version 2.6.0.1
  • the standard library v1.2
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].