We define the notions of a canonical inference rule and a canonical
system in the framework of single-conclusion Gentzen-type systems, and
give a constructive condition for non-triviality of a canonical
system. We develop a general non-deterministic Kripke-style semantics
for such systems, and show that every constructive canonical system
(i.e. coherent canonical single-conclusion system) induces a class of
non-deterministic Kripke-style frames for which it is strongly sound
and complete. We use this non-deterministic semantics to show that all
constructive canonical systems admit a strong form of the
cut-elimination theorem, and to provide a decision procedure for such
systems. These results identify a large family of basic constructive
connectives, including the standard intuitionistic connectives,
together with many other independent connectives.

(Joint work with Arnon Avron.)