The results presented in this paper were obtained in the framework of
basic logic, a new logic aiming at the unification of several logical
systems. The first result is a sequent formulation for orthologic whic
h allows the use of methods of proof theory in quantum logic. Such a f
ormulation admits a very simple procedure of cut-elimination and hence
, because of the subformula property, also a method of proof search an
d an effective decision procedure. By using the framework of basic log
ic, we also obtain a cut-free formulation for orthologic with implicat
ion, for linear orthologic, and, more in generally for a wide range of
new quantum-like logics. These logics meet some requirements expresse
d by physicists and computer scientists. In particular, we propose a g
ood candidate for a linear quantum logic with implication.