Uniformní interpolace a výrokové kvantifikátory v modální logice

Abstrakt

Článek se zabývá uniformními interpolanty v modálních výrokových logikách z důkazově teoretického hlediska, konkrétně prezentuje konstruktivní důkaz uniformní interpolace v modálních logikách K a T poskytující explicitní algoritmus konstrukce interpolantů. Metoda důkazu je založena na simulaci výrokových kvantifikátorů a používá sekventové systémy, umožňující vyhledávání důkazů.

Klíčová slova

• Uniform
• interpolation
• propositional
• quantifiers
• modal
• logics