################################################ # # # README for the script to use paradox/equinox # # # # Stephane Lens # # Janvier 2010 # # Logiques pour l'intelligence artificielle # # Universite de Liege # # Institut Montefiore # # # ################################################ Description of the current modes : ################################################################################ -sat (Test satisfaisability of the input formula) ################################################################################ This mode is provided to test the satisfaisability of an input formula (or a set of formulas). The formula must be encoded in a file in tptp syntax. The formula will be said "Valid", "Satisfiable" or "Unsatisfiable". In the case of a satisfiable formula, the script will give a model of the formula and a model of the negation of the formula. Rem : To test the satisfaisability of a set of formulas, we can separate them with ",\n". Command : "logic -sat fileName" ################################################################################ -csq (Test if conclusion is a logical consequence of the premises) ################################################################################ This mode is provided to test if conclusion is a logical consequence of premises. The file provided to the script must contain some premises and at least one conclusion. To encode one premise we will use "premise{ FORMULA }", and for a conclusion "conclusion{ FORMULA }". With FORMULA the formula in tptp syntax. The rule will be said "Correct" if conclusion is a logical consequence of premises and "Incorrect" otherwise. In the case of an incorrect rule, the script will give a model for which the premises are "true" and the conclusion "false". Command : "logic -csq fileName" ################################################################################ -cmp (Compare set of formulas) ################################################################################ This mode is provided to compare set of formulas. The file provided to the script must contain some formulas that we want to compare in pairs. It is also possible to give some hypothesis to use as axioms when we make the tests. To encode a formula we will use "formula[NAME]{ FORMULA }", and to encode an hypothesis "hyp{ FORMULA }". With NAME the name used to distinguish the formula and FORMULA the formula in tptp syntax. Rem: In hypothesis we can use the "|=", "=|" or "<->" symbols. For each pair the script will respond with one of the following : * A <-> B if A and B are logicaly equivalent ; * A |= B & B |/= A if A is a logical consequence of B but not the opposite ; * A |/= B & B |= A if B is a logical consequence of A but not the opposite ; * A |/= B & B |/= A if there is no logical consequence between the two formulas. For each "A |/= B" the script will give a model for which A is "true" and B is "false". Command : "logic -cmp fileName" ################################################################################ tptp syntax ################################################################################ Usefull part of tptp syntax : formula | formula in tptp syntax -------------------------------------------------------------------------------- a | a NOT a | ~a a OR b | a | b a AND b | a & b a => b | a => b a <= b | a <= b a EQUIV b | a <=> b a XOR b | a <~> b a NAND b | a ~& b a NOR b | a ~| b | FORALLx (A(x) OR B(x)) | ![X] : (a(X) | b(X)) EXISTSx (A(x) AND B(x)) | ?[X] : (a(X) & b(X)) | FORALLxFORALLy (A(x,y) OR B(x,y)) | ![X,Y] : (a(X,Y) | b(X,Y)) |