/*************************************************************************

    File: propTestSuite.pl
    Copyright (C) 2004,2005,2006 Patrick Blackburn & Johan Bos

    This file is part of BB1, version 1.3 (November 2006).

    BB1 is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    BB1 is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with BB1; if not, write to the Free Software Foundation, Inc., 
    59 Temple Place, Suite 330, Boston, MA  02111-1307  USA

*************************************************************************/

:- module(propTestSuite,[formula/2]).


/*========================================================================
   Formulas
========================================================================*/

formula(imp(p, q), 'Not a theorem').

formula(imp(p, p), 'Theorem').

formula(imp(imp(imp(p,q),r),imp(imp(p,q),imp(p,r))), 'Theorem').

formula(imp(p,imp(q,p)), 'Theorem').

formula(imp(imp(p,q),imp(not(q),not(p))), 'Theorem').

formula(imp(imp(not(p),not(q)),imp(q,p)), 'Theorem').

formula(imp(not(not(p)),p), 'Theorem').

formula(imp(p,not(not(p))), 'Theorem').

formula(imp(not(not(not(not(p)))),p), 'Theorem').

formula(imp(p,not(not(not(not(p))))), 'Theorem').

formula(imp(not(or(p,q)),and(not(p),not(q))), 'Theorem').

formula(imp(and(not(p),not(q)),not(or(p,q))), 'Theorem').

formula(imp(not(and(p,q)),or(not(p),not(q))), 'Theorem').

formula(imp(and(not(p),not(q)),not(or(p,q))), 'Theorem').

formula(imp(or(r,and(p,q)),and(or(r,p),or(r,q))), 'Theorem').

formula(imp(and(or(r,p),or(r,q)),or(r,and(p,q))), 'Theorem').

formula(imp(and(r,or(p,q)),or(and(r,p),and(r,q))), 'Theorem').

formula(imp(or(and(r,p),and(r,q)),and(r,or(p,q))), 'Theorem').

formula(imp(and(imp(p,r),imp(q,s)),
            imp(and(p,q),and(r,s))), 'Theorem').

formula(imp(p,or(p,q)), 'Theorem').

formula(imp(p,or(q,p)), 'Theorem').

formula(imp(and(p,q),p), 'Theorem').

formula(imp(and(p,q),q), 'Theorem').

formula(imp(or(p,not(q)),or(p,q)), 'Not a theorem').

formula(imp(and(or(p,not(p)),or(p,not(q))),
            or(p,q)), 'Not a theorem').

formula(imp(and(and(or(p,not(p)),or(r,not(r))),or(p,not(q))),
            or(p,q)), 'Not a theorem').

formula(imp(or(p,and(not(p),q)),or(p,q)), 'Theorem').

formula(and(imp(or(p,and(not(p),q)),or(p,q)),
            imp(or(p,q),or(p,and(not(p),q)))), 'Theorem').


/*------------------------------------------------------------------------
     Pigeonehole principle with 3 pigeons and 2 pigeonholes. 
------------------------------------------------------------------------*/

formula(imp(and(and(or(p11,p12),or(p21,p22)),or(p31,p32)),
            or(or(or(or(or(and(p11,p21),and(p11,p31)),and(p21,p31)),
               and(p12,p22)),and(p12,p32)),and(p22,p32))), 'Theorem').


/*------------------------------------------------------------------------
     The following problem formula codes the pigeonehole principle
     with 4 pigeons and 3 pigeonholes. Neither the tableau nor
     resolution prover terminates on this example. For further
     discussion, see the last section of Chapter 4.
------------------------------------------------------------------------*/

formula(imp(and(and(and(or(or(p11,p12),p13),or(or(p21,p22),p23)),
            or(or(p31,p32),p33)),or(or(p41,p42),p43)),
               or(or(or(or(or(or(or(or(or(or(or(or(or(or(or(or(or(and(p11,p21),
                  and(p11,p31)),and(p11,p41)),and(p21,p31)),and(p21,p41)),
                      and(p31,p41)),and(p12,p22)),and(p12,p32)),and(p12,p42)),
                          and(p22,p32)),and(p22,p42)),and(p32,p42)),and(p13,p23)),
                              and(p13,p33)),and(p13,p43)),and(p23,p33)),
                                  and(p23,p43)),and(p33,p43))), 'Theorem').

formula(imp(and(or(or(or(p11,p12),p13),p14),
                and(or(or(or(p21,p22),p23),p24),
                    and(or(or(or(p31,p32),p33),p34),
                        and(or(or(or(p41,p42),p43),p44),
                            or(or(or(p51,p52),p53),p54))))),
            or(and(p11,p21),
               or(and(p11,p31),
                  or(and(p11,p41),
                     or(and(p11,p51),
                        or(and(p21,p31),
                           or(and(p21,p41),
                              or(and(p21,p51),
                                 or(and(p31,p41),
                                    or(and(p31,p41),
                                       or(and(p41,p51),
                                          or(and(p12,p22),
                                             or(and(p12,p32),
                                                or(and(p12,p42),
                                                   or(and(p12,p52),
                                                      or(and(p22,p32),
                                                         or(and(p22,p42),
                                                            or(and(p22,p52),
                                                               or(and(p32,p42),
                                                                  or(and(p32,p42),
                                                                     or(and(p42,p52),
                                                                        or(and(p13,p23),
                                                                           or(and(p13,p33),
                                                                              or(and(p13,p43),
                                                                                 or(and(p13,p53),
                                                                                    or(and(p23,p33),
                                                                                       or(and(p23,p43),
                                                                                          or(and(p23,p53),
                                                                                             or(and(p33,p43),
                                                                                                or(and(p33,p43),
                                                                                                   or(and(p43,p53),
                                                                                                      or(and(p14,p24),
                                                                                                         or(and(p14,p34),
                                                                                                            or(and(p14,p44),
                                                                                                               or(and(p14,p54),
                                                                                                                  or(and(p24,p34),
                                                                                                                     or(and(p24,p44),
                                                                                                                        or(and(p24,p54),
                                                                                                                           or(and(p34,p44),
                                                                                                                              or(and(p34,p44),
                                                                                                                                 or(and(p44,p54)))))))))))))))))))))))))))))))))))))))))), 'Theorem').
