  Intuitionistic logic extended with decidable propositional atoms combines
classical properties in its propositional part and intuitionistic properties
for derivable formulas not containing propositional symbols. Sequent calculus
is used as a framework for investigating this extension. Admissibility of cut
is retained. Constrained Kripke structures are introduced for modeling
intuitionistic logic with decidable propositional atoms. The extent of the
disjunction and existence properties is investigated. The latest information
about this research can be found at http://sakharov.net/median.html
