diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,4 @@
+0.2.0.0
+-------
+* Separation of the core library (this package) from client code.
+* Substantial simplification of the API and internals.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Author name here (c) 2017
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Author name here nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,16 @@
+# 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).
diff --git a/src/Otter.hs b/src/Otter.hs
new file mode 100644
--- /dev/null
+++ b/src/Otter.hs
@@ -0,0 +1,11 @@
+module Otter
+  ( module Otter.Rule
+  , module Otter.SearchRes
+  , Subsumable(..)
+  , search
+  ) where
+
+import Otter.Rule
+import Otter.SearchRes
+import Otter.Internal.Search
+import Otter.Internal.Structures
diff --git a/src/Otter/Internal/Search.hs b/src/Otter/Internal/Search.hs
new file mode 100644
--- /dev/null
+++ b/src/Otter/Internal/Search.hs
@@ -0,0 +1,128 @@
+{-# LANGUAGE DataKinds #-}
+
+module Otter.Internal.Search where
+
+import Data.Bifunctor (second)
+import Data.Maybe
+import Control.Monad.State.Lazy
+import Data.Foldable
+import Control.Applicative
+
+import Otter.Rule
+import Otter.Internal.Structures
+import Otter.SearchRes
+
+data ProverState n = PS
+  { _rules :: [SearchProperRule n]
+  , _actives :: ActiveNodes n
+  , _inactives :: InactiveNodes n
+  , _index :: GlobalIndex n
+  , _isGoal :: n -> Bool
+  }
+
+type Prover s g a = State (ProverState s) a
+
+-- | Result type of matching a list of rules to an input sequent.
+type RuleAppRes n = ([ConclNode n], [SearchProperRule n])
+
+popInactive :: Prover s g (Maybe (ActiveNode s))
+popInactive = do
+  (PS r as is gi g) <- get
+  case popInactiveOp is of
+    Just (newIs, inactive) -> do
+      let (newAs, active) = activate as inactive
+      put (PS r newAs newIs gi g)
+      return (Just active)
+    Nothing -> return Nothing
+
+getActives :: Prover s g (ActiveNodes s)
+getActives = _actives <$> get
+
+getRules :: Prover s g [SearchProperRule s]
+getRules = _rules <$> get
+
+isGoalM :: FSCheckedNode s -> Prover s g (Maybe (FSCheckedNode s))
+isGoalM s = do
+  g <- fmap _isGoal get
+  if g (extractNode s) then pure (Just s) else pure Nothing
+
+haveGoal :: [FSCheckedNode s] -> Prover s g (Maybe (FSCheckedNode s))
+haveGoal = fmap (foldr (<|>) mzero) . mapM isGoalM
+
+filterUnsubsumed
+  :: Subsumable s
+  => [ConclNode s] -> Prover s g [SearchNode FSChecked s]
+filterUnsubsumed = fmap catMaybes . mapM isNotFwdSubsumed
+
+isNotFwdSubsumed
+  :: Subsumable s
+  => ConclNode s -> Prover s g (Maybe (SearchNode FSChecked s))
+isNotFwdSubsumed concl = fmap (flip fwdSubsumes concl . _index) get
+
+removeSubsumedBy
+  :: Subsumable s
+  => SearchNode FSChecked s -> Prover s g (SearchNode BSChecked s)
+removeSubsumedBy fschecked = do
+  (PS r as is gi g) <- get
+  let (newIs, bschecked) = removeSubsumedByOp fschecked is
+  put (PS r as newIs gi g)
+  return bschecked
+
+addRule :: SearchProperRule s -> Prover s g ()
+addRule r = do
+  (PS rls as is gi g) <- get
+  put (PS (r : rls) as is gi g)
+
+addInactive :: SearchNode BSChecked s -> Prover s g ()
+addInactive i = do
+  (PS r as is gi g) <- get
+  let (newIs, newInd) = addToInactives is gi i
+  put (PS r as newIs newInd g)
+
+percolate :: ActiveNodes s -> [SearchProperRule s] -> RuleAppRes s
+percolate _ [] = mempty
+percolate actives rules = r1 `mappend` r2
+  where
+    activeList = foldActives toList actives
+    r1 = foldMap (uncurry apply) ((,) <$> rules <*> activeList)
+    r2 = percolate actives . snd $ r1
+
+processNewActive :: ActiveNode s -> Prover s g (RuleAppRes s)
+processNewActive node = do
+  actives <- getActives
+  rules <- getRules
+  let r1 = foldMap (`apply` node) rules
+      r2 = percolate actives . snd $ r1
+  return $ r1 <> r2
+
+merge :: Maybe (SearchNode s a) -> SearchRes a -> SearchRes a
+merge m sr = maybe (delay sr) (\x -> cons (extractNode x) sr) m
+
+loop :: Subsumable s => Prover s g (SearchRes s)
+loop = do
+  inactive <- popInactive
+  case inactive of
+    Nothing -> pure []
+    Just node -> do
+      res <- processNewActive node
+      unsubSeqs <- filterUnsubsumed (fst res)
+      unsubSeqs' <- mapM removeSubsumedBy unsubSeqs
+      mapM_ addInactive unsubSeqs'
+      mapM_ addRule (snd res)
+      liftM2 merge (haveGoal unsubSeqs) loop
+
+doSearch
+  :: Subsumable s
+  => [SearchNode Initial s] -> [SearchProperRule s] -> Prover s g (SearchRes s)
+doSearch initSeqs initRls = do
+  mapM_ addInactive (fmap initIsBSCheckd initSeqs)
+  mapM_ addRule initRls
+  liftM2 merge (haveGoal (fmap initIsFSCheckd initSeqs)) loop
+
+search
+  :: Subsumable s
+  => [s] -> [s -> Rule s s] -> (s -> Bool) -> (SearchRes s, [s])
+search initial rls isGl = second (toList . _index) $
+  runState
+    (doSearch (fmap initialize initial) (fmap toProperRule rls))
+    (PS [] emptyActives emptyInactives emptyGI isGl)
diff --git a/src/Otter/Internal/Structures.hs b/src/Otter/Internal/Structures.hs
new file mode 100644
--- /dev/null
+++ b/src/Otter/Internal/Structures.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE GADTs #-}
+
+module Otter.Internal.Structures
+  ( Stage(..)
+  , SearchNode
+  , ActiveNode
+  , FSCheckedNode
+  , BSCheckedNode
+  , InactiveNode
+  , ActiveNodes
+  , InactiveNodes
+  , ConclNode
+  , GlobalIndex
+  , SearchRule
+  , SearchProperRule
+  , Subsumable(..)
+  -- , OrdSearchGoal(..)
+  -- , applyRule
+  , initIsFSCheckd
+  , initIsBSCheckd
+  , initialize
+  -- , subsumesGoalOp
+  , removeSubsumedByOp
+  , fwdSubsumes
+  , activate
+  , popInactiveOp
+  , addToInactives
+  , foldActives
+  , mkGoal
+  , emptyActives
+  , emptyInactives
+  , emptyGI
+  , toProperRule
+  , extractNode
+  )
+   where
+
+import Otter.Rule
+
+class Subsumable n where
+  subsumes :: n -> n -> Bool
+
+-- | Stages of proof search
+data Stage
+  = Initial    -- ^ Initial node
+  | Active     -- ^ Active node
+  | Inactive   -- ^ Inactive node
+  | Concl      -- ^ Conclusion node
+  | FSChecked  -- ^ Forward subsumption-checked
+  | BSChecked  -- ^ Backward subsumption-checked
+  | GlIndex    -- ^ Global index node
+  | Goal       -- ^ Goal node
+
+-- | Type of search nodes in the search space, given by
+-- a node together with a proof search stage.
+data SearchNode :: Stage -> * -> * where
+  InitN :: seq -> SearchNode Initial seq
+  ActiveN :: seq -> SearchNode Active seq
+  InactiveN :: seq -> SearchNode Inactive seq
+  ConclN :: seq -> SearchNode Concl seq
+  FSCheckedN :: seq -> SearchNode FSChecked seq
+  BSCheckedN :: seq -> SearchNode BSChecked seq
+  GoalN :: seq -> SearchNode Goal seq
+
+deriving instance Show a => Show (SearchNode s a)
+
+extractNode :: SearchNode s seq -> seq
+extractNode (InitN s) = s
+extractNode (ActiveN s) = s
+extractNode (InactiveN s) = s
+extractNode (ConclN s) = s
+extractNode (BSCheckedN s) = s
+extractNode (FSCheckedN s) = s
+extractNode (GoalN s) = s
+
+type ActiveNode n = SearchNode Active n
+type BSCheckedNode n = SearchNode BSChecked n
+type FSCheckedNode n = SearchNode FSChecked n
+newtype ActiveNodes n = AS [SearchNode Active n]
+type InactiveNode n = SearchNode Inactive n
+newtype InactiveNodes n = IS [InactiveNode n]
+
+type ConclNode n = SearchNode Concl n
+data GlobalIndex n = GI !Int ![n]
+
+instance Foldable GlobalIndex where
+  foldr f z (GI _ l) = foldr f z l
+
+--------------------------------------------------------------------------------
+
+initialize :: n -> SearchNode Initial n
+initialize = InitN
+
+initIsFSCheckd :: SearchNode Initial n -> FSCheckedNode n
+initIsFSCheckd (InitN s) = FSCheckedN s
+
+initIsBSCheckd :: SearchNode Initial n -> BSCheckedNode n
+initIsBSCheckd (InitN s) = BSCheckedN s
+
+mkGoal :: n -> SearchNode Goal n
+mkGoal = GoalN
+
+emptyActives :: ActiveNodes n
+emptyActives = AS mempty
+
+emptyInactives :: InactiveNodes n
+emptyInactives = IS mempty
+
+emptyGI :: GlobalIndex n
+emptyGI = GI 0 mempty
+
+--------------------------------------------------------------------------------
+
+{-| Type of elements that represent the result of applying an inference rule.
+
+    Such application may either fail, succeed with a value (when the rule has
+    been fully applied), or succeed with a function (when the rule is only
+    partially applied and has still some premises to match). -}
+type SearchRule n = Rule (ActiveNode n) (ConclNode n)
+
+{-| Type of inference rules.
+    Axioms are not considered rules in this case, so a rule takes at least one
+    premise. Hence the corresponding type is a function from a premise sequent
+    to a rule application result. -}
+type SearchProperRule n = ProperRule (ActiveNode n) (ConclNode n)
+
+toProperRule :: (n -> Rule n n) -> SearchProperRule n
+toProperRule = arrowDimap extractNode (relDimap extractNode ConclN)
+
+--------------------------------------------------------------------------------
+-- Operations
+
+foldActives
+  :: (forall f. Foldable f => f (ActiveNode n) -> b) -> ActiveNodes n -> b
+foldActives folder (AS actives) = folder actives
+
+activate
+  :: ActiveNodes n -> InactiveNode n -> (ActiveNodes n, ActiveNode n)
+activate (AS as) (InactiveN s) = (AS (ActiveN s : as), ActiveN s)
+
+popInactiveOp
+  :: InactiveNodes n -> Maybe (InactiveNodes n, InactiveNode n)
+popInactiveOp (IS is) =
+  case is of
+    (x : xs) -> Just (IS xs, x)
+    [] -> Nothing
+
+addToInactives
+  :: InactiveNodes n -> GlobalIndex n -> BSCheckedNode n
+  -> (InactiveNodes n, GlobalIndex n)
+addToInactives (IS ins) (GI n gi) (BSCheckedN s) =
+  (IS (InactiveN s : ins), GI (n + 1) (s : gi))
+
+fwdSubsumes
+  :: Subsumable n
+  => GlobalIndex n -> SearchNode Concl n -> Maybe (FSCheckedNode n)
+fwdSubsumes (GI _ globalIndex) (ConclN s) =
+  if any (`subsumes` s) globalIndex
+    then Nothing
+    else Just (FSCheckedN s)
+
+removeSubsumedByOp
+  :: Subsumable n
+  => FSCheckedNode n -> InactiveNodes n -> (InactiveNodes n, BSCheckedNode n)
+removeSubsumedByOp (FSCheckedN s) (IS is) =
+  let ff = filter filterer is
+  in (IS ff, BSCheckedN s)
+  where filterer = not . (s `subsumes`) . extractNode
diff --git a/src/Otter/Rule.hs b/src/Otter/Rule.hs
new file mode 100644
--- /dev/null
+++ b/src/Otter/Rule.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE DerivingVia #-}
+
+module Otter.Rule where
+
+import Data.Bifunctor (bimap)
+import Control.Monad (MonadPlus(..))
+import Control.Monad.Fail (MonadFail(..))
+import Control.Applicative (Alternative(..), WrappedMonad(..))
+
+{-| An inference rule schema is just a curried n-ary function where n is an
+    unbounded, unspecified number of input premises, possibly zero (in that
+    case, the rule is an axiom). A 'Rule' element may represent three possible
+    situations:
+
+    1. A failing computation which produces nothing; this is the degenerate case
+       of a rule schema that always fails to match, and also what enables to
+       make 'Rule' an instance of 'Alternative', 'MonadPlus', and 'MonadFail'.
+    2. A successful computation that produces a 0-ary function, i.e. an axiom;
+    3. A successful computation that produces a unary function, that is,
+       a function accepting one argument and possibly returning a new 'Rule'.
+       Applying such a function to an input corresponds to "matching"
+       the first premise of the rule schema against a candidate input.
+       The result is either a matching failure or a new, partially applied
+       rule.
+ -}
+newtype Rule a b = Rule { unRule :: Maybe (Either b (a -> Rule a b)) }
+  deriving (Functor, Applicative) via WrappedMonad (Rule a)
+type ProperRule a b = a -> Rule a b
+
+-- | Constructs a single-premise rule from a matching function. 
+match :: (a -> Maybe b) -> Rule a b
+match p = Rule . Just . Right $ Rule . fmap Left . p
+
+apply :: ProperRule a b -> a -> ([b], [ProperRule a b])
+apply f = maybe mempty (either ((,[]) . pure) (([],) . pure)) . unRule . f
+
+instance Monad (Rule a) where
+  return = Rule . Just . Left
+  (Rule rel) >>= f =
+    Rule $ rel >>= either (unRule . f) (Just . Right . fmap (>>= f))
+
+instance Alternative (Rule a) where
+  empty = Rule Nothing
+  (Rule Nothing) <|> rel = rel
+  rel <|> _ = rel
+
+instance MonadPlus (Rule a) where
+
+instance MonadFail (Rule a) where
+  fail _ = Rule Nothing
+
+arrowDimap :: (a -> b) -> (c -> d) -> (b -> c) -> (a -> d)
+arrowDimap f g h x = g (h (f x))
+
+-- This is just 'dimap' from the 'Profunctor' typeclass, but defined here
+-- standalone to avoid pulling in profunctors for just a couple of uses of
+-- 'dimap'.
+relDimap :: (a -> b) -> (c -> d) -> Rule b c -> Rule a d
+relDimap f g = Rule . fmap (bimap g (arrowDimap f (relDimap f g))) . unRule
diff --git a/src/Otter/SearchRes.hs b/src/Otter/SearchRes.hs
new file mode 100644
--- /dev/null
+++ b/src/Otter/SearchRes.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE DeriveFunctor #-}
+
+module Otter.SearchRes
+  ( SearchRes
+  , Res(..)
+  , Extraction(..)
+  , FailureReason(..)
+  , extractResults
+  , delay
+  , cons
+  ) where
+
+import Data.List.NonEmpty (NonEmpty(..))
+
+data Res a = Res a | Delay deriving (Functor)
+
+-- | Type representing the result of proof search. Every element in the list
+-- corresponds to the result of analysing node in the search space by the search
+-- algorithm. The result is 'Res' in the positive case the node is a goal node,
+-- or 'Delay' in the negative case.
+--
+-- The search agorithm produces an element of `'SearchRes' a` lazily, inserting
+-- 'Delay' constructors to ensure that the computation is productive even in the
+-- case no goal node is found in the search space. This allows to perform proof
+-- search in an on-demand fashion, possibly giving up after a certain number of
+-- 'Delay's.
+type SearchRes a = [Res a]
+
+-- | Delays a search result stream.
+--
+-- @
+-- delay x == Delay : x
+-- @
+delay :: SearchRes a -> SearchRes a
+delay = (Delay :)
+
+-- | Appends a result to a search result stream.
+--
+-- @
+-- cons x y = Res x : y
+-- @
+cons :: a -> SearchRes a -> SearchRes a
+cons x = (Res x :)
+
+-- | Type of reasons why no result can be extracted from a search result stream.
+-- 
+-- Either the search space has been exhaustively searched and no result was
+-- found (the query is not a theorem), or the search was terminated preemptively
+-- according to an upper bound imposed on the maximum depth of the search space.
+data FailureReason = NotATheorem | SpaceTooBig
+
+-- | Type of the result of 'extractResults', which extracts all positive search
+-- results from a search result stream.
+-- An element of `Extraction a` is either a non-empty list of positive results,
+-- or an element of 'SpaceExhausted' giving a reason why no result was found.
+data Extraction a = AllResults (NonEmpty a) | NoResults FailureReason
+
+resListUntil :: Int -> SearchRes a -> ([a], FailureReason)
+resListUntil _ [] = ([], NotATheorem)
+resListUntil 0 (_ : _)  = ([], SpaceTooBig)
+resListUntil i (Res x : xs) = let (ys, b) = resListUntil i xs in (x : ys, b)
+resListUntil i (Delay : xs) = resListUntil (i - 1) xs
+
+-- | Extract all the positive results from a search result stream, stopping if
+-- no result is found after the given number of delays.
+extractResults :: Int -> SearchRes a -> Extraction a
+extractResults i res = case resListUntil i res of
+  ([], b) -> NoResults b
+  (x : xs, _) -> AllResults (x :| xs)
+  
diff --git a/src/Zsyntax.hs b/src/Zsyntax.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax.hs
@@ -0,0 +1,56 @@
+{-# LANGUAGE TypeOperators #-}
+
+module Zsyntax
+  ( module Zsyntax.Formula
+  , search
+  , searchLabelled
+  , toLabelledGoal
+  , O.SearchRes
+  , O.Extraction(..)
+  , O.FailureReason(..)
+  , DecoratedLSequent
+  , Label
+  , O.extractResults
+  ) where
+
+import qualified Otter as O
+import Zsyntax.Formula
+import Zsyntax.Labelled.Rule.Interface
+import Zsyntax.Labelled.Rule
+import Zsyntax.Labelled.DerivationTerm
+import Data.Foldable
+import Control.Monad.State
+import Data.Maybe (mapMaybe)
+
+type DecoratedLSequent a l = DerivationTerm a l ::: LSequent a l
+type Label = Int
+
+-- | Turns a sequent into a labelled sequent that is suitable for proof search,
+-- by breaking the linear context formulas into neutral formulas, and
+-- labelling all subformulas with unique labels.
+toLabelledGoal :: Ord a => Sequent a -> GoalNSequent a Label
+toLabelledGoal s = evalState (neutralize s) 0
+
+-- | Searches for a derivation of the specified sequent.
+--
+-- @
+-- search g == searchLabelled (toLabelledGoal g)
+-- @
+search :: Ord a
+       => Sequent a
+       -> ( O.SearchRes (DecoratedLSequent a Label)
+          , [DecoratedLSequent a Label])
+search = searchLabelled . toLabelledGoal
+
+-- | Searches for a derivation of the specified goal sequent.
+-- Returns the search results, as well as all searched sequents.
+searchLabelled :: Ord a
+       => GoalNSequent a Label
+       -> ( O.SearchRes (DecoratedLSequent a Label)
+          , [DecoratedLSequent a Label])
+searchLabelled goal = O.search (toList seqs) rules isGoal
+  where
+    initial = initialRules goal
+    seqs    = mapMaybe maySequent initial
+    rules   = mapMaybe mayProperRule initial
+    isGoal s' = (toGoalSequent . _payload $ s') `O.subsumes` goal
diff --git a/src/Zsyntax/Formula.hs b/src/Zsyntax/Formula.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax/Formula.hs
@@ -0,0 +1,180 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
+
+module Zsyntax.Formula where
+  -- (
+  --   -- * Biochemical formulas
+  --   BioFormula(..)
+  -- , ppBioFormula
+  -- -- * Logical formulas
+  -- , Axiom
+  -- , axiom
+  -- , axiom'
+  -- , axForget
+  -- , Formula
+  -- , atom
+  -- , conj
+  -- , impl
+  -- , ppFormula
+  -- -- * Sequents
+  -- , Sequent(..)
+  -- , neutralize
+  -- ) where
+
+import Control.Arrow ((>>>))
+import Data.Bifunctor (second)
+import Zsyntax.Labelled.Formula
+import Zsyntax.Labelled.Rule (Neutral(..),GoalNSequent(..))
+-- import Data.MultiSet.NonEmpty
+import Data.MultiSet (MultiSet, fromList)
+import Data.Foldable (toList)
+import Data.Set (Set)
+import qualified Data.Set as S (fromList)
+import Data.List.NonEmpty (NonEmpty(..), sort)
+import Control.Monad.State
+import Data.Either (partitionEithers)
+import Data.Function (on)
+
+--------------------------------------------------------------------------------
+-- Biochemical atomic formulas
+
+{-| Type of biochemical (non-logical) formulas, which constitute
+    the logical atoms of logical formulas of Zsyntax.
+    It is parameterized over the type of biochemical atoms. -}
+data BioFormula a = BioAtom a
+                  | BioInter (BioFormula a) (BioFormula a)
+                  deriving (Functor, Foldable, Traversable, Show)
+
+instance Semigroup (BioFormula a) where
+  (<>) = BioInter
+
+normalize :: Ord a => BioFormula a -> NonEmpty a
+normalize (BioAtom x) = x :| []
+normalize (BioInter f1 f2) = sort (normalize f1 <> normalize f2)
+
+-- | Custom equality instance for biological atoms.
+-- It includes commutativity of the biological interaction operator.
+instance Ord a => Eq (BioFormula a) where
+  (==) = on (==) normalize
+
+instance Ord a => Ord (BioFormula a) where
+  compare = on compare normalize
+
+-- | Pretty-prints biochemical formulas, given a way to pretty print its atoms.
+--
+-- @
+-- >>> ppBioFormula id (BioAtom "foo" <> BioAtom "bar" <> BioAtom "baz")
+-- "((foo ⊙ bar) ⊙ baz)"
+-- @
+ppBioFormula :: (a -> String) -> BioFormula a -> String
+ppBioFormula p (BioAtom x) = p x
+ppBioFormula p (BioInter x y) =
+  "(" ++ ppBioFormula p x ++ " ⊙ " ++ ppBioFormula p y ++ ")"
+
+--------------------------------------------------------------------------------
+-- Simple formulas
+
+-- | Type of logical axioms of Zsyntax.
+newtype Axiom a = Axiom { unSA :: LAxiom a () }
+  deriving Show
+
+axForget :: LAxiom a l -> Axiom a
+axForget = Axiom . void
+
+-- | Constructs an axiom from non-empty lists of logical atoms as premise and
+-- conclusion.
+axiom :: NonEmpty a -> ReactionList a -> NonEmpty a -> Axiom a
+axiom prms cty concl = axiom' (f prms) cty (f concl)
+  where f = foldl1 (bConj ()) . fmap BAtom
+
+axiom' :: BFormula a () -> ReactionList a -> BFormula a () -> Axiom a
+axiom' b1 r b2 = Axiom (LAx b1 r b2 ())
+
+-- | Type of logical formulas of Zsyntax, parameterized by the type of atoms
+-- (which are typically 'BioFormula's).
+data Formula a = forall k . Formula (LFormula k a ())
+
+-- | Pretty-prints Zsyntax formulas, given a way to pretty-print its atoms.
+ppFormula :: (a -> String) -> Formula a -> String
+ppFormula p (Formula f) = ppLFormula p f
+-- TODO: wut?
+-- @
+-- >>> ppFormula id (impl (conj (atom "foo") (atom "bar")) mempty mempty (atom "baz"))
+-- "(foo \8855 bar \8594 baz)"
+-- @
+
+deriving instance Show a => Show (Formula a)
+
+instance Ord a => Eq (Formula a) where
+  (Formula f1) == (Formula f2) = deepHetComp f1 f2 == EQ
+
+instance Ord a => Ord (Formula a) where
+  compare (Formula f1) (Formula f2) = deepHetComp f1 f2
+
+instance Ord a => Eq (Axiom a) where
+  (Axiom ax1) == (Axiom ax2) = deepHetComp (axToFormula ax1) (axToFormula ax2) == EQ
+
+instance Ord a => Ord (Axiom a) where
+  compare (Axiom ax1) (Axiom ax2) = deepHetComp (axToFormula ax1) (axToFormula ax2)
+
+-- | Constructs an atomic formula from a logical atom.
+atom :: a -> Formula a
+atom = Formula . Atom
+
+lToS :: LFormula k a l -> Formula a
+lToS = Formula . void
+
+-- | Constructs the conjunction of two formulas.
+conj :: Formula a -> Formula a -> Formula a
+conj (Formula f1) (Formula f2) = lToS (Conj f1 f2 ())
+
+-- | Constructs a Zsyntax conditional (aka linear implication) between two
+-- formulas, whose associated biochemical reaction is described by a given
+-- elementary base and reaction list.
+impl :: Formula a -> ElemBase a -> ReactionList a -> Formula a -> Formula a
+impl (Formula f1) eb cs (Formula f2) = Formula (Impl f1 eb cs f2 ())
+
+--------------------------------------------------------------------------------
+-- Sequents
+
+-- | Type of ZBS sequents.
+data Sequent a =
+  SQ { _sqUC    :: Set (Axiom a)
+     , _sqLC    :: MultiSet (Formula a)
+     , _sqConcl :: (Formula a)
+     }
+  deriving Show
+
+nuLabel :: (Enum l, MonadState l m) => m l
+nuLabel = do { s <- get ; put (succ s) ; return s }
+
+-- | Turns a sequent into a labelled goal sequent.
+neutralize
+  :: (MonadState l m, Enum l, Ord a, Ord l)
+  => Sequent a -> m (GoalNSequent a l)
+neutralize (SQ unrestr linear (Formula concl)) = GNS <$> ul <*> ln <*> nGoal
+  where
+    ul = fmap S.fromList . mapM (traverse (const nuLabel) . unSA)
+       . toList $ unrestr
+    ln = fmap (fromList . join) . mapM neutralizeFormula . toList $ linear
+    nGoal = O <$> traverse (const nuLabel) concl
+
+maybeNeutral :: Opaque a l -> Either (Neutral a l) [Opaque a l]
+maybeNeutral (O f@(Atom _)) = Left (N f)
+maybeNeutral (O (Conj a b _)) = Right [O a, O b]
+maybeNeutral (O f@Impl{}) = Left (N f)
+
+neutralizeOs :: (Ord a, Ord l) => [Opaque a l] -> [Neutral a l]
+neutralizeOs [] = []
+neutralizeOs xs =
+  uncurry (<>) . second (neutralizeOs . join) .
+    partitionEithers . fmap maybeNeutral $ xs
+
+neutralizeFormula
+  :: (MonadState l m, Enum l, Ord a, Ord l) => Formula a -> m [Neutral a l]
+neutralizeFormula = labelSF >>> fmap (return >>> neutralizeOs)
+  where labelSF (Formula f) = fmap O . traverse (const nuLabel) $ f
diff --git a/src/Zsyntax/Labelled/DerivationTerm.hs b/src/Zsyntax/Labelled/DerivationTerm.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax/Labelled/DerivationTerm.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Zsyntax.Labelled.DerivationTerm where
+
+import Zsyntax.Labelled.Formula
+
+-- | Derivation term of the labelled forward sequent calculus.
+data DerivationTerm a l where
+  Init  :: a -> DerivationTerm a l
+  Copy  :: DerivationTerm a l -> LAxiom a l -> DerivationTerm a l
+  ConjR :: DerivationTerm a l -> DerivationTerm a l -> l -> DerivationTerm a l
+  ConjL :: DerivationTerm a l -> DerivationTerm a l
+  ImplR :: DerivationTerm a l -> LFormula k a l -> ElemBase a -> ReactionList a -> l
+        -> DerivationTerm a l
+  ImplL :: DerivationTerm a l -> DerivationTerm a l -> LFormula k a l
+        -> DerivationTerm a l
+
+deriving instance Functor (DerivationTerm a)
+
+concl :: DerivationTerm a l -> Opaque a l
+concl (Init a) = O (Atom a)
+concl (Copy d _) = concl d
+concl (ConjR d d' l) = O (oConj (concl d) (concl d') l)
+concl (ConjL d) = concl d
+concl (ImplR d a eb cty l) = O (oImpl (O a) eb cty (concl d) l)
+concl (ImplL _ d' _) = concl d'
+
+transitions :: DerivationTerm a l -> [(Opaque a l, Opaque a l)]
+transitions (Init _) = []
+transitions (Copy d _) = transitions d
+transitions (ConjR d1 d2 _) = transitions d1 ++ transitions d2
+transitions (ConjL d) = transitions d
+transitions (ImplR d _ _ _ _) = transitions d
+transitions (ImplL d1 d2 b) = transitions d1 ++ [(concl d1, O b)] ++ transitions d2
diff --git a/src/Zsyntax/Labelled/Formula.hs b/src/Zsyntax/Labelled/Formula.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax/Labelled/Formula.hs
@@ -0,0 +1,296 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
+
+module Zsyntax.Labelled.Formula
+  ( FKind(..)
+  , Label(..)
+  , ElemBase(..)
+  , ReactionList
+  -- * Labelled formulas
+  , LFormula(..)
+  , ppLFormula
+  , elemBase
+  , label
+  , frmlHetEq
+  , frmlHetOrd
+  , deepHetComp
+  -- * Labelled axioms
+  , LAxiom(..)
+  , axLabel
+  , axToFormula
+  , ppLAxiom
+  -- * Opaque formulas
+  , Opaque(..)
+  , withOpaque
+  , oConj
+  , oImpl
+  -- * Basic formulas
+  , BFormula(..)
+  , bAtom
+  , bConj
+  , bfToFormula
+  , bfToAtoms
+  , maybeBFormula
+  ) where
+
+import Zsyntax.ReactionList
+import Data.MultiSet (MultiSet, singleton)
+import Data.Foldable (fold)
+import Data.List.NonEmpty (NonEmpty(..))
+
+newtype ElemBase a = ElemBase { unEB :: MultiSet a }
+  deriving (Semigroup, Monoid, Eq, Ord, Show)
+
+data FKind = KAtom | KConj | KImpl
+
+type ReactionList a = RList (ElemBase a) (CtrlSet a)
+
+-- | Type of labelled formulas, indexed by a formula kind and parameterized by
+-- the type of the labels and of the logical atoms.
+data LFormula :: FKind -> * -> * -> * where
+  Atom :: a -> LFormula KAtom a l
+  Conj
+    :: LFormula k1 a l
+    -> LFormula k2 a l
+    -> l
+    -> LFormula KConj a l
+  Impl
+    :: LFormula k1 a l
+    -> ElemBase a
+    -> ReactionList a
+    -> LFormula k2 a l
+    -> l
+    -> LFormula KImpl a l
+
+deriving instance (Show a, Show l) => Show (LFormula k a l)
+
+-- | Heterogeneous equality test between labelled formulas.
+--
+-- This function just compares the formulas' labels for equality, under the
+-- assumption that labels have been assigned in a sensible way.
+frmlHetEq :: (Eq a, Eq l) => LFormula k1 a l -> LFormula k2 a l -> Bool
+frmlHetEq f1 f2 = label f1 == label f2
+
+-- | Heterogeneous comparison between labelled formulas.
+--
+-- This function just compares the formulas' labels, under the assumption that
+-- labels have been assigned in a sensible way.
+frmlHetOrd :: (Ord a, Ord l) => LFormula k1 a l -> LFormula k2 a l -> Ordering
+frmlHetOrd f1 f2 = compare (label f1) (label f2)
+
+foldF
+  :: (a -> b)
+  -> (b -> b -> l -> b)
+  -> (b -> ElemBase a -> ReactionList a -> b -> l -> b)
+  -> LFormula k a l -> b
+foldF f _ _ (Atom a) = f a
+foldF f g h (Conj f1 f2 l) = g (foldF f g h f1) (foldF f g h f2) l
+foldF f g h (Impl f1 eb cty f2 l) = h (foldF f g h f1) eb cty (foldF f g h f2) l
+
+deriving instance Functor (LFormula k a)
+deriving instance Foldable (LFormula k a)
+deriving instance Traversable (LFormula k a)
+
+-- | Pretty-print labelled formulas, given a way to pretty-print its atoms.
+--
+-- Note that this function ignores labels, for which one should use the 'Show'
+-- instance.
+ppLFormula :: (a -> String) -> LFormula k a l -> String
+ppLFormula p = foldF p (\a b _ -> fold [a, " ⊗ ", b])
+                     (\a _ _ b _ -> fold ["(", a, " → ", b, ")"])
+
+-- | Returns the elementary base of a labelled formula.
+elemBase :: Ord a => LFormula k a l -> ElemBase a
+elemBase = foldF (ElemBase . singleton) (\a b _ -> a <> b) (\_ e _ _ _ -> e)
+
+--------------------------------------------------------------------------------
+-- Opaque formulas
+
+-- | Type of opaque formulas, that is, those for which we do not care about
+-- their formula kind.
+data Opaque a l = forall k . O (LFormula k a l)
+
+deriving instance (Show a, Show l) => Show (Opaque a l)
+
+instance (Eq l, Eq a) => Eq (Opaque a l) where
+  O f1 == O f2 = frmlHetEq f1 f2
+
+instance (Ord l, Ord a) => Ord (Opaque a l) where
+  compare (O f1) (O f2) = frmlHetOrd f1 f2
+
+withOpaque :: (forall k . LFormula k a l -> b) -> Opaque a l -> b
+withOpaque f (O fr) = f fr
+
+-- | Constructs the conjunction of two opaque formulas. The result is a provably
+-- conjunctive labelled formula.
+oConj :: Opaque a l -> Opaque a l -> l -> LFormula KConj a l
+oConj (O f1) (O f2) = Conj f1 f2
+
+-- | Constructs the Zsyntax conditional (aka linear implication) between two
+-- opaque formulas, whose reaction is described by a given elementary base and
+-- reaction list. The result is a provably implicational labelled formula.
+oImpl :: Opaque a l -> ElemBase a -> ReactionList a -> Opaque a l -> l
+      -> LFormula KImpl a l
+oImpl (O f1) eb cty (O f2) = Impl f1 eb cty f2
+
+--------------------------------------------------------------------------------
+-- Basic formulas
+
+-- | Type of basic formulas.
+-- A basic formula is one composed of conjunctions of atoms.
+data BFormula a l = BAtom a | BConj (BFormula a l) (BFormula a l) l
+  deriving (Functor, Foldable, Traversable, Show)
+
+-- | Constructs a basic formula from a logical atom.
+bAtom :: a -> BFormula a l
+bAtom = BAtom
+
+-- | Constructs the conjunction of two basic formulas, with a given label.
+bConj :: l -> BFormula a l -> BFormula a l -> BFormula a l
+bConj l f1 f2 = BConj f1 f2 l
+
+-- data ExBFormula a l = forall k . ExBFormula (LFormula k a l)
+
+-- | Returns the labelled formula corresponding to a given basic formula.
+--
+-- Note that the result formula is opaque, since it could be an atom as well as
+-- a conjunction, and thus has no determined index.
+bfToFormula :: BFormula a l -> Opaque a l
+bfToFormula (BAtom x) = O (Atom x)
+bfToFormula (BConj f1 f2 l) = O (oConj (bfToFormula f1) (bfToFormula f2) l)
+
+-- | Unrolls a basic formula, discarding all labels and returning a (non-empty)
+-- list of all its constituent logical atoms.
+bfToAtoms :: BFormula a l -> NonEmpty a
+bfToAtoms (BAtom bf) = bf :| []
+bfToAtoms (BConj f1 f2 _) = bfToAtoms f1 <> bfToAtoms f2
+
+-- | Decides whether the input labelled formula is a basic formula, and if so,
+-- it returns it wrapped in 'Just' as a proper basic formula.
+maybeBFormula :: LFormula k a l -> Maybe (BFormula a l)
+maybeBFormula (Atom x) = pure (BAtom x)
+maybeBFormula (Conj f1 f2 l) =
+  BConj <$> maybeBFormula f1 <*> maybeBFormula f2 <*> pure l
+maybeBFormula Impl {} = Nothing
+-- was: decideF
+
+--------------------------------------------------------------------------------
+
+data LAxiom a l = LAx (BFormula a l) (ReactionList a) (BFormula a l) l
+  deriving (Show, Functor, Foldable, Traversable)
+
+-- | Converts a labelled axiom to a labelled formula.
+axToFormula :: Ord a => LAxiom a l -> LFormula KImpl a l
+axToFormula (LAx f1 _ f2 l) = case (bfToFormula f1, bfToFormula f2) of
+  (O f1', O f2') ->
+    Impl (mapCty (const mempty) f1') mempty mempty (mapCty (const mempty) f2') l
+
+-- | Pretty-prints a labelled axiom, given a way to pretty-print its atoms.
+--
+-- Note that this function ignores labels, for which one should rely on the
+-- 'Show' instance.
+ppLAxiom :: Ord a => (a -> String) -> LAxiom a l -> String
+ppLAxiom p ax = ppLFormula p (axToFormula ax)
+
+-- | Type of formula labels. Note that logical atoms are their own labels.
+data Label a l
+  = L l -- ^ Regular label
+  | A a -- ^ Logical atom
+  deriving (Eq, Ord, Show)
+
+-- | Returns the label of a labelled axiom.
+axLabel :: LAxiom a l -> l
+axLabel (LAx _ _ _ l) = l
+
+-- | Returns the label of a labelled formula.
+label :: LFormula k a l -> Label a l
+label = foldF A (\_ _ -> L) (\_ _ _ _ -> L)
+
+--------------------------------------------------------------------------------
+-- Mapping functions
+
+-- mapAtoms :: Ord a' => (a -> a') -> LFormula k a l -> LFormula k a' l
+-- mapAtoms f (Atom a) = Atom (f a)
+-- mapAtoms f (Conj a b l) = Conj (mapAtoms f a) (mapAtoms f b) l
+-- mapAtoms f (Impl a e c b l) =
+--   Impl (mapAtoms f a) (over pack (MS.map f) e) c (mapAtoms f b) l
+
+mapCty :: (ReactionList a -> ReactionList a) -> LFormula k a l -> LFormula k a l
+mapCty _ (Atom a) = Atom a
+mapCty f (Conj f1 f2 l) = Conj (mapCty f f1) (mapCty f f2) l
+mapCty f (Impl f1 eb cty f2 l) = Impl (mapCty f f1) eb (f cty) (mapCty f f2) l
+
+-- mapCtyAx :: (cty1 -> cty2) -> LAxiom a l -> LAxiom a l
+-- mapCtyAx f (LAx f1 cty f2 l) = LAx f1 (f cty) f2 l
+
+--------------------------------------------------------------------------------
+-- Deep heterogeneous comparison functions
+
+isEq :: Ordering -> Either Ordering Ordering
+isEq x = if x == EQ then Right x else Left x
+
+-- | Returns the result of a deep heterogeneous comparison between two labelled formulas.
+--
+-- Comparison is "deep" in the sense that is considers the entire recursive
+-- structure of formulas. This is unlike 'frmlHetOrd', which only compares
+-- labels.
+deepHetComp
+  :: (Ord a, Ord l)
+  => LFormula k1 a l -> LFormula k2 a l -> Ordering
+deepHetComp (Atom x1) (Atom x2) = compare x1 x2
+deepHetComp (Atom _) _ = LT
+deepHetComp (Conj a1 b1 l1) (Conj a2 b2 l2) =
+  either id id $ isEq ca >> isEq cb >> pure cl
+  where ca = deepHetComp a1 a2 ; cb = deepHetComp b1 b2 ; cl = compare l1 l2
+deepHetComp Conj{} (Atom _) = GT
+deepHetComp Conj{} Impl{} = LT
+deepHetComp (Impl a1 eb1 cs1 b1 l1) (Impl a2 eb2 cs2 b2 l2) =
+  either id id $ isEq ca >> isEq cb >> isEq ceb >> isEq ccs >> pure cl
+  where
+    ca = deepHetComp a1 a2 ; cb = deepHetComp b1 b2 ; ceb = compare eb1 eb2
+    ccs = compare cs1 cs2 ; cl = compare l1 l2
+deepHetComp Impl{} _ = GT
+
+--------------------------------------------------------------------------------
+
+-- -- | Type of labelled formulas to be used during proof search.
+-- newtype SrchFormula a l k = Srch { unSrch :: LFormula k a l }
+
+-- instance (Show a, Show l) => Show1 (SrchFormula a l) where
+--   show1 (Srch f) = show f
+
+-- instance (Ord a, Ord l) => HEq (SrchFormula cty a l) where
+--   hetCompare (Srch f1) (Srch f2) = compare (label f1) (label f2)
+
+instance Eq l => Eq (LAxiom a l) where
+  ax1 == ax2 = axLabel ax1 == axLabel ax2
+
+instance Ord l => Ord (LAxiom a l) where
+  compare ax1 ax2 = compare (axLabel ax1) (axLabel ax2)
+
+-- type instance Atom (SrchFormula cty a l) = a
+-- type instance Eb (SrchFormula cty a l) = ElemBase a
+-- type instance Ax (SrchFormula cty a l) = LAxiom cty a l
+
+-- sfrmlView :: SrchFormula cty a l k
+--           -> FrmlView (SrchFormula cty a l) k (ElemBase a) cty a
+-- sfrmlView (Srch (Atom a)) = AtomRepr a
+-- sfrmlView (Srch (Conj f1 f2 _)) = ConjRepr (Srch f1) (Srch f2)
+-- sfrmlView (Srch (Impl f1 e c f2 _)) = ImplRepr (Srch f1) e c (Srch f2)
+
+-- decideN :: Neutral (SrchFormula cty a l) -> Maybe (BFormula a l)
+-- decideN = switchN (\(Srch (Atom x)) -> Just (BAtom x)) (const Nothing)
+
+-- decideOF :: Opaque (SrchFormula cty a l) -> Maybe (BFormula a l)
+-- decideOF (O (Srch f)) = decideF f
diff --git a/src/Zsyntax/Labelled/Rule.hs b/src/Zsyntax/Labelled/Rule.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax/Labelled/Rule.hs
@@ -0,0 +1,12 @@
+module Zsyntax.Labelled.Rule
+  ( module Zsyntax.Labelled.Rule.Interface
+  -- * Bipole generation
+  , module Zsyntax.Labelled.Rule.BipoleRelation
+  -- * Initial sequents and rules generation
+  , module Zsyntax.Labelled.Rule.Frontier
+  ) where
+
+import Zsyntax.Labelled.Rule.BipoleRelation
+import Zsyntax.Labelled.Rule.Frontier
+import Zsyntax.Labelled.Rule.Interface
+  -- (UCtxt, LCtxt, LSequent(..), NeutralKind, Neutral(..), withNeutral, lcBase)
diff --git a/src/Zsyntax/Labelled/Rule/BipoleRelation.hs b/src/Zsyntax/Labelled/Rule/BipoleRelation.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax/Labelled/Rule/BipoleRelation.hs
@@ -0,0 +1,152 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+
+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
+{-| Module of derived rule relations. -}
+
+module Zsyntax.Labelled.Rule.BipoleRelation where
+  -- ( (:::)
+  -- , AnnLSequent
+  -- , IsFocusable
+  -- , BipoleRule
+  -- , focus
+  -- , implLeft
+  -- , copyRule
+  -- , implRight
+  -- ) where
+
+import Data.Function (on)
+import Data.Bifunctor (Bifunctor(..))
+import Control.Monad (guard)
+
+import Otter
+import Data.Set (insert)
+import Data.MultiSet (MultiSet, isSubsetOf, (\\), singleton)
+import qualified Data.MultiSet as MS (insert)
+
+import Zsyntax.Labelled.Rule.Interface
+import Zsyntax.Labelled.Formula
+import Zsyntax.Labelled.DerivationTerm
+import Zsyntax.ReactionList
+
+respects :: Ord a => ElemBase a -> RList (ElemBase a) (CtrlSet a) -> Bool
+respects = respectsRList (\eb cty -> msRespectsCS (unEB eb) cty)
+
+--------------------------------------------------------------------------------
+
+-- | Type of derivation terms-decorated data.
+data tm ::: pl = (:::) { _term :: tm, _payload :: pl } deriving (Eq, Ord, Show)
+
+instance Bifunctor (:::) where
+  bimap f g (x ::: y) = f x ::: g y
+
+-- | Type of labelled sequents that are annotated with a derivation term.
+type AnnLSequent a l = DerivationTerm a l ::: LSequent a l
+
+-- | A relation is an unbounded curried function with an annotated sequents as
+-- input.
+type BipoleRel a l = Rule (AnnLSequent a l)
+
+-- | A rule of the derived rule calculus is a relation that has
+-- derivation term-decorated sequents as both input and output.
+type BipoleRule a l = Rule (AnnLSequent a l) (AnnLSequent a l)
+
+-- | Predicate identifying those formula kinds that correspond to focusable
+-- formulas.
+class IsFocusable (k :: FKind) where
+instance IsFocusable KAtom where
+instance IsFocusable KConj where
+
+type FocMatchRes a l = MatchRes a l FullXiEmptyResult
+type DTFocMatchRes a l = DerivationTerm a l ::: FocMatchRes a l
+type DTMatchRes a l actcase = DerivationTerm a l ::: MatchRes a l actcase
+
+instance Subsumable s => Subsumable (tm ::: s) where
+  subsumes = subsumes `on` _payload
+
+--------------------------------------------------------------------------------
+
+-- | Given two multisets m1 and m2, it checks whether m1 is contained in m2,
+-- and returns the rest of m2 if it is the case.
+matchMultiSet :: Ord a => MultiSet a -> MultiSet a -> Maybe (MultiSet a)
+matchMultiSet m1 m2 = if isSubsetOf m1 m2 then Just (m2 \\ m1) else Nothing
+
+matchLinearCtxt
+  :: (Ord a, Ord l) => SchemaLCtxt a l -> LCtxt a l -> Maybe (LCtxt a l)
+matchLinearCtxt (SLC slc) = matchMultiSet slc
+
+matchSchema :: (Ord a, Ord l)
+            => SSchema a l act -> AnnLSequent a l -> Maybe (DTMatchRes a l act)
+matchSchema (SSEmptyGoal delta) (term ::: LS gamma delta' cty goal) = do
+  delta'' <- matchLinearCtxt delta delta'
+  pure (term ::: MRFullGoal gamma delta'' cty goal)
+matchSchema (SSFullGoal delta cty cncl) (tm ::: LS gamma delta' cty' cncl') = do
+  delta'' <- matchLinearCtxt delta delta'
+  guard (cty == cty')
+  guard (cncl == cncl')
+  pure (tm ::: MREmptyGoal gamma delta'')
+
+matchRel :: (Ord a, Ord l)
+         => LCtxt a l -> ZetaXi a l act -> BipoleRel a l (DTMatchRes a l act)
+matchRel delta zetaxi = match . matchSchema $
+  case zetaxi of
+    EmptyZetaXi -> SSEmptyGoal (SLC delta)
+    FullZetaXi cty g -> SSFullGoal (SLC delta) cty g
+
+positiveFocalDispatch
+  :: (Ord l, Ord a)
+  => LFormula k a l
+  -> BipoleRel a l (DTFocMatchRes a l)
+positiveFocalDispatch fr = case fr of
+  Atom a -> pure (Init a ::: MREmptyGoal mempty (singleton (N fr)))
+  Impl {} -> match (matchSchema (SSFullGoal (SLC mempty) mempty (O fr)))
+  Conj f1 f2 l -> do
+    d ::: MREmptyGoal g1 d1 <- positiveFocalDispatch f1
+    d' ::: MREmptyGoal g2 d2 <- positiveFocalDispatch f2
+    pure $ ConjR d d' l ::: MREmptyGoal (g1 <> g2) (d1 <> d2)
+
+leftActive
+  :: (Ord l, Ord a) => LCtxt a l -> [Opaque a l] -> ZetaXi a l act
+  -> BipoleRel a l (DTMatchRes a l act)
+leftActive delta [] zetaxi = matchRel delta zetaxi
+leftActive delta (O f : rest) zetaxi = withMaybeNeutral f
+  (leftActive (MS.insert (N f) delta) rest zetaxi)
+  (\(Conj f1 f2 _) -> do
+      d ::: res <- leftActive delta (O f2 : O f1 : rest) zetaxi
+      pure $ ConjL d ::: res)
+
+focus :: (Ord l, Ord a, IsFocusable k) => LFormula k a l -> BipoleRule a l
+focus formula = do
+  d ::: MREmptyGoal gamma delta <- positiveFocalDispatch formula
+  pure (d ::: LS gamma delta mempty (O formula))
+
+implLeft :: (Ord l, Ord a) => LFormula KImpl a l -> BipoleRule a l
+implLeft fr@(Impl f1 _ cty f2 _) = do
+  d  ::: MREmptyGoal g1 d1 <- positiveFocalDispatch f1
+  d' ::: MRFullGoal g2 d2 cty' cl <- leftActive mempty [(O f2)] EmptyZetaXi
+  let b = lcBase d2
+      ext = extend b cty
+  guard (respects b cty)
+  pure $ ImplL d d' f2
+     ::: LS (g1 <> g2) (MS.insert (N fr) (d1 <> d2)) (ext <> cty') cl
+
+copyRule :: (Ord a, Ord l) => LAxiom a l -> BipoleRule a l
+copyRule ax = let fr = axToFormula ax in case fr of
+  Impl f1 _ cty f2 _ -> do
+    d  ::: MREmptyGoal g1 d1 <- positiveFocalDispatch f1
+    d' ::: MRFullGoal g2 d2 cty' cl <- leftActive mempty [(O f2)] EmptyZetaXi
+    let b = lcBase d2 ; ext = extend b cty
+    guard (respects b cty)
+    pure $ Copy (ImplL d d' f2) ax
+       ::: LS (insert ax (g1 <> g2)) (d1 <> d2) (ext <> cty') cl
+
+implRight :: (Ord a, Ord l) => LFormula KImpl a l -> BipoleRule a l
+implRight fr@(Impl f1 eb cty f2 l) = do
+  tm ::: MREmptyGoal g d <- leftActive mempty [(O f1)] (FullZetaXi cty (O f2))
+  guard (lcBase d == eb)
+  pure $ ImplR tm fr eb cty l ::: LS g d mempty (O fr)
diff --git a/src/Zsyntax/Labelled/Rule/Frontier.hs b/src/Zsyntax/Labelled/Rule/Frontier.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax/Labelled/Rule/Frontier.hs
@@ -0,0 +1,133 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+
+module Zsyntax.Labelled.Rule.Frontier where
+  -- ( GoalNSequent(..)
+  -- , Rule
+  -- , initialSequentsAndRules
+  -- ) where
+
+import Data.Maybe (mapMaybe)
+import Data.Constraint (Dict(..))
+import Otter (unRule, Subsumable(..))
+import Data.MultiSet (MultiSet)
+import Data.Foldable (toList)
+import Data.Set (Set)
+import qualified Data.Set as S (singleton, fromList)
+import Data.Function (on)
+import Control.Monad (join)
+
+import Zsyntax.Labelled.Rule.BipoleRelation
+import Zsyntax.Labelled.Rule.Interface
+import Zsyntax.Labelled.Formula
+
+data DecoratedFormula :: * -> * -> * where
+  Unrestr :: LAxiom a l -> DecoratedFormula a l
+  LinNeg :: LFormula KImpl a l -> DecoratedFormula a l
+  LinPos :: Opaque a l -> DecoratedFormula a l
+
+dfLabel :: DecoratedFormula a l -> Label a l
+dfLabel (Unrestr ax) = L (axLabel ax)
+dfLabel (LinNeg f) = label f
+dfLabel (LinPos (O f)) = label f
+
+instance (Eq l, Eq a) => Eq (DecoratedFormula a l) where
+  (==) = on (==) dfLabel
+
+instance (Ord l, Ord a) => Ord (DecoratedFormula a l) where
+  compare = on compare dfLabel
+
+--------------------------------------------------------------------------------
+-- Goal and result sequents.
+
+-- | Type of goal sequents.
+--
+-- A goal sequent is characterized by an unrestricted context of axioms, a
+-- (non-empty) neutral context, and a consequent formula of unspecified formula
+-- kind (i.e., an opaque formula).
+data GoalNSequent a l = GNS
+  { _gnsUC :: Set (LAxiom a l)
+  , _gnsLC :: MultiSet (Neutral a l) -- NonEmptyMultiSet (Neutral a l)
+  , _gnsConcl :: Opaque a l -- Opaque (LFormula' cty l l)
+  }
+  deriving Show
+
+instance (Ord a, Ord l) => Subsumable (GoalNSequent a l) where
+  subsumes  (GNS uc lc fr) (GNS uc' lc' fr') =
+    fr == fr' && lc == lc' && null (_scOnOnlyFirst (uc `subCtxtOf` uc'))
+
+toGoalSequent :: LSequent a l -> GoalNSequent a l
+toGoalSequent (LS uc lc _ c) = GNS uc lc c
+
+--------------------------------------------------------------------------------
+ -- Frontier computation
+
+filterImpl :: [Neutral a l] -> [LFormula 'KImpl a l]
+filterImpl = mapMaybe aux
+  where
+    aux :: Neutral a l -> Maybe (LFormula 'KImpl a l)
+    aux (N (f :: LFormula k a l)) =
+      either (const Nothing) (\Dict -> Just f) (decideNeutral @k)
+
+frNeg :: (Ord l, Ord a) => Neutral a l -> Set (DecoratedFormula a l)
+frNeg = switchN (const mempty) (\(Impl a _ _ b _) -> foc a <> act b)
+
+frPos, foc, act :: (Ord l, Ord a) => LFormula k a l -> Set (DecoratedFormula a l)
+frPos f = case f of
+  Atom _ -> mempty
+  Conj {} -> foc f
+  Impl a _ _ b _ -> mconcat [act a, frPos b, S.singleton (LinPos (O b))]
+foc f = case f of
+  Atom _ -> mempty
+  Conj a b _ -> foc a <> foc b
+  Impl {} -> S.singleton (LinPos (O f)) <> frPos f
+act f = case f of
+  Atom _ -> mempty
+  Conj f1 f2 _ -> act f1 <> act f2
+  Impl {} -> S.singleton (LinNeg f) <> frPos f
+
+-- | Computes the frontier of a sequent.
+frontier :: (Ord l, Ord a) => GoalNSequent a l -> Set (DecoratedFormula a l)
+frontier (GNS uc lc goal@(O fgoal)) =
+  mconcat 
+    [ toplevelUC, toplevelLC
+    , ucFrontier, linFrontier
+    , goalFrontier, S.singleton (LinPos goal)
+    ]
+  where
+    lcList = toList lc
+    toplevelUC = S.fromList . map Unrestr . toList $ uc
+    toplevelLC = S.fromList . fmap LinNeg . filterImpl $ lcList
+    ucFrontier = mconcat . fmap (frNeg . N . axToFormula) . toList $ uc
+    linFrontier = mconcat . fmap frNeg $ lcList
+    goalFrontier = frPos fgoal
+
+--------------------------------------------------------------------------------
+-- Generation of initial rules from the frontier.
+
+generateRule :: (Ord a, Ord l) => DecoratedFormula a l -> BipoleRule a l
+generateRule (Unrestr axiom) = copyRule axiom
+generateRule (LinNeg impl) = implLeft impl
+generateRule (LinPos (O f)) =
+  case f of { Atom _ -> focus f ; Conj {} -> focus f ; Impl {} -> implRight f }
+  
+--------------------------------------------------------------------------------
+-- Main function
+
+-- | Type of proper rules of the formal system, i.e. 'BipoleRule's that take at
+-- least one premise.
+type ProperRule a l = AnnLSequent a l -> BipoleRule a l
+
+-- | Computes the set of initial rules from the frontier of a specified goal
+-- sequent.
+initialRules :: (Ord a, Ord l) => GoalNSequent a l -> [BipoleRule a l]
+initialRules = fmap generateRule . toList . frontier
+
+mayProperRule :: BipoleRule a l -> Maybe (ProperRule a l)
+mayProperRule = join . fmap (either (const Nothing) Just) . unRule
+
+maySequent :: BipoleRule a l -> Maybe (AnnLSequent a l)
+maySequent = join . fmap (either Just (const Nothing)) . unRule
diff --git a/src/Zsyntax/Labelled/Rule/Interface.hs b/src/Zsyntax/Labelled/Rule/Interface.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax/Labelled/Rule/Interface.hs
@@ -0,0 +1,186 @@
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE GADTs #-}
+
+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors -Wno-orphans -Wno-unused-imports #-}
+
+module Zsyntax.Labelled.Rule.Interface where
+
+import Otter (Subsumable(..))
+import Data.Foldable (toList)
+import Data.List (intersperse)
+import Data.Set (Set, (\\), isSubsetOf)
+import Data.Map (Map)
+import Data.Maybe (fromMaybe)
+import qualified Data.Map as M (lookup)
+import Zsyntax.Labelled.Formula
+import Data.Constraint (Dict(..))
+import Data.MultiSet (MultiSet)
+import Data.Function (on)
+
+-- import Core.FormulaKind
+-- import Formula
+-- import LinearContext
+
+--------------------------------------------------------------------------------
+-- Neutral sequents
+
+-- -- | Type of unrestricted contexts. Unrestricted contexts are made out of
+-- -- elements of some type of axiomatic formulas.
+-- type UCtxt = Set Ax
+-- -- | Type of linear contexts. Linear contexts are made out of neutral formulas.
+-- type LCtxt = LinearCtxt -- (Neutral Frml)
+
+-- data NSequent' cty = NS
+--   { _nsUC :: UCtxt
+--   , _nsLC :: LCtxt
+--   , _nsCty :: cty
+--   , _nsConcl :: Opaque Frml
+--   } deriving (Functor)
+
+-- type NSequent = NSequent' Cty
+
+-- prettyNS :: NSequent -> String
+-- prettyNS (NS _ lc _ c) =
+--   concat (intersperse "," (fmap (withNeutral prettyF) (lcList lc))) ++ " ==> " ++
+--   withOpaque prettyF c
+
+-- deriving instance Eq cty => Eq (NSequent' cty)
+-- deriving instance Ord cty => Ord (NSequent' cty)
+
+--------------------------------------------------------------------------------
+-- Labelled sequents
+
+-- | Type of labelled unrestricted contexts, i.e. sets of labelled axioms.
+type UCtxt a l = Set (LAxiom a l)
+
+-- | Type of labelled neutral contexts, i.e. multisets of neutral labelled
+-- formulas.
+type LCtxt a l = MultiSet (Neutral a l)
+
+-- | Type of labelled sequents.
+data LSequent a l = LS
+  { lsUCtxt :: UCtxt a l
+  , lsLCtxt :: LCtxt a l
+  , lsCty :: ReactionList a
+  , lsConcl :: Opaque a l
+  }
+
+data SubCtxt a = SC
+  { _scOnOnlyFirst :: [a]
+  , _scRestFirst :: [a]
+  }
+
+subCtxtOf :: Ord a => Set a -> Set a -> SubCtxt a
+subCtxtOf s1 s2 =
+  if isSubsetOf s1 s2 then SC [] (toList s1) else SC (toList df) df'
+  where df = s1 \\ s2 ; df' = toList (s1 \\ df)
+
+instance (Ord a, Ord l) => Subsumable (LSequent a l) where
+  subsumes  (LS uc lc c fr) (LS uc' lc' c' fr') =
+    fr == fr' && lc == lc' && c == c' && null (_scOnOnlyFirst (uc `subCtxtOf` uc'))
+
+--------------------------------------------------------------------------------
+-- Neutral formulas.
+
+-- | Predicate identifying those formula kinds corresponding to neutral
+-- formulas.
+class NeutralKind (k :: FKind) where
+  decideNeutral :: Either (Dict (k ~ KAtom)) (Dict (k ~ KImpl))
+instance NeutralKind KAtom where decideNeutral = Left Dict
+instance NeutralKind KImpl where decideNeutral = Right Dict
+
+-- | Type of neutral formulas, i.e. all formulas whose formula kind is
+-- classified as neutral by 'NeutralKind'.
+data Neutral a l = forall k . NeutralKind k => N (LFormula k a l)
+
+deriving instance (Show a, Show l) => Show (Neutral a l)
+
+withMaybeNeutral
+  :: LFormula k a l
+  -> (NeutralKind k => b)
+  -> (LFormula KConj a l -> b)
+  -> b
+withMaybeNeutral fr f g = case fr of
+  Atom {} -> f
+  Impl {} -> f
+  Conj {} -> g fr
+
+withNeutral :: (forall k. NeutralKind k => LFormula k a l -> b) -> Neutral a l -> b
+withNeutral f (N fr) = f fr
+
+switchN :: (LFormula KAtom a l -> b) -> (LFormula KImpl a l -> b) -> Neutral a l -> b
+switchN f g (N (x :: LFormula k a l)) =
+  either (\Dict -> f x) (\Dict -> g x) (decideNeutral @k)
+
+-- class Show1 (fr :: k -> *) where show1 :: fr a -> String
+-- instance Show (Opaque a l) where show (O f) = "O " ++ show1 f
+-- instance Show (Neutral a l) where show (N f) = "N " ++ show1 f
+
+instance (Eq l, Eq a) => Eq (Neutral a l) where
+  N f1 == N f2 = frmlHetEq f1 f2
+
+instance (Ord l, Ord a) => Ord (Neutral a l) where
+  compare (N f1) (N f2) = frmlHetOrd f1 f2
+
+--------------------------------------------------------------------------------
+
+-- | Linear contexts that appear in sequent schemas.
+newtype SchemaLCtxt a l = SLC (LCtxt a l)
+
+deriving instance (Ord l, Ord a) => Semigroup (SchemaLCtxt a l)
+-- deriving instance Monoid SchemaLCtxt
+
+{-| Type indicating the possible shapes of an active relation.
+    An active relation has the form
+
+      act(delta ; omega ==>_zeta xi)[...] -> gamma' ; delta' -->> res
+
+    where either
+    1. xi is a formula, zeta is a control set, and res is empty, or
+    2. xi is empty, zeta is empty, and res is a formula. -}
+data ActCase = FullXiEmptyResult | EmptyXiFullResult
+
+-- | Sequent schemas.
+data SSchema :: * -> * -> ActCase -> * where
+  SSEmptyGoal :: SchemaLCtxt a l -> SSchema a l EmptyXiFullResult
+  SSFullGoal
+    :: SchemaLCtxt a l
+    -> ReactionList a
+    -> Opaque a l
+    -> SSchema a l FullXiEmptyResult
+
+-- | Pre-sequents to be used as match results.
+data MatchRes :: * -> * -> ActCase -> * where
+  MREmptyGoal :: UCtxt a l -> LCtxt a l -> MatchRes a l FullXiEmptyResult
+  MRFullGoal
+    :: UCtxt a l -> LCtxt a l -> ReactionList a -> Opaque a l
+    -> MatchRes a l EmptyXiFullResult
+
+data ZetaXi :: * -> * -> ActCase -> * where
+  FullZetaXi
+    :: ReactionList a
+    -> Opaque a l
+    -> ZetaXi a l FullXiEmptyResult
+  EmptyZetaXi :: ZetaXi a l EmptyXiFullResult
+
+--------------------------------------------------------------------------------
+-- Elementary bases and control sets
+
+elemBaseAll :: (Foldable f, Ord a) => f (Opaque a l) -> ElemBase a
+elemBaseAll = mconcat . fmap (withOpaque elemBase) . toList
+  
+lcBase :: Ord a => LCtxt a l -> ElemBase a
+lcBase = foldMap (withNeutral elemBase)
diff --git a/src/Zsyntax/ReactionList.hs b/src/Zsyntax/ReactionList.hs
new file mode 100644
--- /dev/null
+++ b/src/Zsyntax/ReactionList.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Zsyntax.ReactionList where
+
+-- import Core.LinearContext
+import Data.Set (Set)
+import qualified Data.Set as S (map,fromList)
+import Data.Bifunctor (first)
+import Data.Foldable (toList)
+import Data.MultiSet (MultiSet, isSubsetOf)
+-- import Data.MultiSet.NonEmpty
+
+data CtrlType = Regular | SupersetClosed deriving (Eq, Ord, Show)
+data CtrlSetCtxt af = CSC
+  { _cscType :: CtrlType
+  , _cscCtxt :: MultiSet af
+  } deriving (Eq, Ord, Show)
+
+{-| A control set is a set of linear contexts made up of atomic formulas, that is,
+    multisets of formulas of the bonding language.
+
+    For a context C in a control set S we may want to consider its superset
+    closure, that is, have that C' is in S for all superset C' of C.
+    We therefore distinguish between superset-closed contexts and normal
+    contexts in a control set. Actually, superset-closed contexts are the only
+    way to specify infinite control sets.
+-}
+newtype CtrlSet af = CS
+  { unCS :: Set (CtrlSetCtxt af)
+  } deriving (Eq, Ord, Semigroup, Monoid, Show)
+
+fromCSCtxts :: (Foldable f, Ord af) => f (CtrlSetCtxt af) -> CtrlSet af
+fromCSCtxts = CS . S.fromList . toList
+
+toCtxtList :: CtrlSet af -> [CtrlSetCtxt af]
+toCtxtList = toList . unCS
+
+-- | Checks whether a linear context "respects" a control set context.
+respectsCC :: Ord af => MultiSet af -> CtrlSetCtxt af -> Bool
+respectsCC ms (CSC Regular ctxt) = ms /= ctxt
+respectsCC ms (CSC SupersetClosed ctxt) = not (ctxt `isSubsetOf` ms)
+
+-- | Checks whether a linear context "respects" a control set, that is,
+-- if it respects all the control set contexts.
+msRespectsCS :: Ord af => MultiSet af -> CtrlSet af  -> Bool
+msRespectsCS ms = and . S.map (respectsCC ms) . unCS
+
+-- | A reaction list is a list of pairs, where in each pair the first component
+-- is an elementary base, and the second component is a control set.
+newtype RList eb cs = RL
+  { unRL :: [(eb, cs)]
+  } deriving (Eq, Ord, Semigroup, Monoid, Show)
+
+justCS :: Monoid eb => cs -> RList eb cs
+justCS cs = RL [(mempty, cs)]
+
+-- | Extends a reaction list with an elementary base.
+extend :: Semigroup eb => eb -> RList eb cs -> RList eb cs
+extend base = RL . map (first (base <>)) . unRL
+-- was: extendRList
+
+-- | Checks whether an elementary base "respects" a reaction list, given
+-- a function to check whether the base "respects" the list's control sets.
+respectsRList :: Semigroup eb => (eb -> cs -> Bool) -> eb -> RList eb cs -> Bool
+respectsRList resp base = and . fmap (uncurry resp . first (base <>)) . unRL
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,50 @@
+import Zsyntax
+import qualified Otter as O
+import System.Exit (exitFailure)
+import qualified Data.Set as S (fromList)
+import qualified Data.MultiSet as M
+import Data.List.NonEmpty (fromList)
+import Zsyntax.ReactionList
+
+type Atom = BioFormula String
+
+main :: IO ()
+main = checkSequent goal
+
+checkSequent :: Sequent Atom -> IO ()
+checkSequent g =
+  case O.extractResults 2000 (fst $ search (toLabelledGoal g)) of
+    O.AllResults _ -> putStrLn "test passed."
+    O.NoResults _  -> putStrLn "test failed." >> exitFailure
+
+ax :: Ord a => [a] -> [a] -> [a] -> Axiom (BioFormula a)
+ax xs ys rl =
+  axiom (fromList $ fmap BioAtom xs)
+        (justCS $ fromCSCtxts [CSC SupersetClosed
+                                (M.fromList (fmap BioAtom rl))])
+        (fromList $ fmap BioAtom ys)
+
+goal :: Sequent Atom
+goal = SQ (S.fromList axioms) (M.fromList from) to
+  where
+    axioms :: [Axiom Atom]
+    axioms =
+      [ ax ["ICL"] ["MUS81"] mempty
+      , ax ["MUS81", "FANCD21"] ["FAN1"] mempty
+      , ax ["FANCM", "ATR"] ["FAcore"] ["CHKREC"]
+      , ax ["FANCM", "ATM"] ["FAcore"] ["CHKREC"]
+      , ax ["FAcore", "ATM"] ["FANCD21"] ["USP1"]
+      , ax ["FAcore", "ATR"] ["FANCD21"] ["USP1"]
+      , ax ["FAcore", "H2AX", "DSB"] ["FANCD21"] ["USP1"]
+      , ax ["ICL"] ["FANCM"] ["CHKREC"]
+      , ax ["FAN1"] ["DSB"] ["HRR", "NHEJ"]
+      , ax ["XPF"] ["DBS"] ["HRR", "NHEJ"]
+      , ax ["MUS81", "FAN1"] ["ADD"] ["PCNATLS"]
+      , ax ["ATM"] ["ATM", "ATM"] mempty
+      , ax ["ICL"] ["ICL", "ICL"] mempty
+      ]
+    from :: [Formula Atom]
+    from = [atom (BioAtom "ICL"), atom (BioAtom "ATM")]
+    to :: Formula Atom
+    to = conj (atom (BioAtom "DSB")) (atom (BioAtom "ADD"))
+
diff --git a/zsyntax.cabal b/zsyntax.cabal
new file mode 100644
--- /dev/null
+++ b/zsyntax.cabal
@@ -0,0 +1,91 @@
+name:           zsyntax
+version:        0.2.0.0
+description:    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>).
+
+category:       Logic, Theorem Provers, Bioinformatics
+synopsis:       Automated theorem prover for the Zsyntax biochemical calculus
+homepage:       https://github.com/fsestini/zsyntax#readme                 
+bug-reports:    https://github.com/fsestini/zsyntax/issues
+author:         Filippo Sestini
+maintainer:     sestini.filippo@gmail.com
+copyright:      2018 Filippo Sestini
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+cabal-version:  2
+
+extra-source-files:
+    README
+    CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/fsestini/zsyntax
+
+library
+
+  exposed-modules:
+      Zsyntax
+      Zsyntax.Formula
+      Zsyntax.ReactionList
+
+      Zsyntax.Labelled.Rule
+      Zsyntax.Labelled.Formula
+      Zsyntax.Labelled.DerivationTerm
+
+      Zsyntax.Labelled.Rule.BipoleRelation
+      Zsyntax.Labelled.Rule.Frontier
+      Zsyntax.Labelled.Rule.Interface
+
+      Otter
+      Otter.Rule
+      Otter.SearchRes
+      Otter.Internal.Search
+      Otter.Internal.Structures
+
+  default-extensions:
+      LambdaCase
+      TupleSections
+  hs-source-dirs: src
+  ghc-options:
+      -Wall
+      -Wcompat
+      -Wincomplete-record-updates
+      -Wincomplete-uni-patterns
+      -Wredundant-constraints
+      -Wno-unticked-promoted-constructors
+      -- -Werror
+  build-depends:
+      base >=4.7 && <5
+    , constraints >= 0.10.1 && < 0.11
+    , containers >= 0.6.0 && < 0.7
+    , multiset >= 0.3.4 && < 0.4
+    , mtl >= 2.2.2 && < 2.3
+  default-language: Haskell2010
+
+test-suite zsyntax-test
+  type:             exitcode-stdio-1.0
+  hs-source-dirs:   test
+  build-depends:    base >=4.7 && <5
+                  , zsyntax
+                  , containers >= 0.6.0 && < 0.7
+                  , multiset >= 0.3.4 && < 0.4
+                  , mtl >= 2.2.2 && < 2.3
+  main-is:          Main.hs
+  default-language: Haskell2010