zsyntax: Automated theorem prover for the Zsyntax biochemical calculus

[ bioinformatics, bsd3, library, logic, theorem-provers ] [ Propose Tags ]

An automated theorem prover for Zsyntax, a logical calculus for molecular biology inspired by linear logic, that can be used to automatically verify biological pathways expressed as logical sequents. The prover implements automatic proof search for the Zsyntax sequent calculus (ZBS), a logical calculus for a context-sensitive fragment of multiplicative linear logic where sequents are decorated so to account for the biochemical constraints. The theory behind the Zsyntax sequent calculus and its proof search procedure is developed in F. Sestini, S. Crafa, Proof-search in a context-sensitive logic for molecular biology, Journal of Logic and Computation, 2018 (https://doi.org/10.1093/logcom/exy028).


[Skip to Readme]
Versions [faq] 0.2.0.0
Change log CHANGELOG.md
Dependencies base (>=4.7 && <5), constraints (>=0.10.1 && <0.11), containers (>=0.6.0 && <0.7), mtl (>=2.2.2 && <2.3), multiset (>=0.3.4 && <0.4) [details]
License BSD-3-Clause
Copyright 2018 Filippo Sestini
Author Filippo Sestini
Maintainer sestini.filippo@gmail.com
Category Logic, Theorem Provers, Bioinformatics
Home page https://github.com/fsestini/zsyntax#readme
Bug tracker https://github.com/fsestini/zsyntax/issues
Source repo head: git clone https://github.com/fsestini/zsyntax
Uploaded by fsestini at Sat Dec 15 13:06:11 UTC 2018
Distributions NixOS:0.2.0.0
Downloads 92 total (13 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2018-12-15 [all 1 reports]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees


Readme for zsyntax-0.2.0.0

[back to package description]
# zsyntax core library

This library is a Haskell implementation of an automated theorem
prover for Zsyntax, a logical calculus for molecular biology inspired
by linear logic, that can be used to automatically verify biological
pathways expressed as logical sequents.

The prover implements fully-automatic forward proof search for the
Zsyntax sequent calculus (ZBS), a logical calculus for a
context-sensitive fragment of multiplicative linear logic where
sequents are decorated so to account for the biochemical constraints.

The theory behind the Zsyntax sequent calculus and its proof search
procedure is developed in F. Sestini, S. Crafa, Proof-search in a
context-sensitive logic for molecular biology, Journal of Logic and
Computation, 2018 (https://doi.org/10.1093/logcom/exy028).