Для пропозиційної логіки сформульовано дві стратегії, задані у формі спеціальних секвенційних числень. Наведено деякі результати щодо їхньої коректності та повноти, та проведено порівняння запропонованих числень. Показано, що жодне з них не має перевагинад іншим з точки зору побудови мінімальних виводів.