A theorem prover for Conditional Logics

Nested Sequent calculi for normal conditional logics in Prolog by Nicola Olivetti and Gian Luca Pozzato, with the help of Cyril Terrioux

Check the validity of a conditional formula

Conditional logic

CK
  • + ID
  • + MP
  • + CEM
  • + CSO

Do NOT use capital letters for propositional variables. Use:
  • false for bottom
  • true for top
  • ^ for conjunction
  • v for disjunction
  • ! for negation
  • -> for material implication
  • => for conditional implication

CK+CEM+MP(+ID), CK+CSO(+MP+CEM) are not available.
Remember that flat CK+ID+CSO=cumulative logic C

Testing NESCOND's performances

NESCOND's performances are promising. We have compared them with the ones of CondLean's and GoalDUCK's. For the flat fragment of CK+CSO+ID we have compared NESCOND with KLMLean, a theorem prover for KLM logics. Here are some statistics from our experiments.

Test over random formulas
Percentage of timeouts running NESCOND, CondLean and GoalDUCK over 2000 randomnly generated formulas with a 10 seconds time limit.
Test over valid formulas: CK
Percentage of timeouts running NESCOND and CondLean over 88 CK valid seqents.
Test over valid formulas: extensions of CK
Percentage of timeouts running NESCOND and CondLean over 52 valid seqents for extensions of CK.
NESCOND vs KLMLean (CK+CSO+ID)
Percentage of timeouts running NESCOND and KLMlean over 1000 random formulas.

Files for testing NESCOND's performances

Description Document
Test for CK: NESCOND vs CondLean vs UCK Prolog code
Test for extensions of CK: valid formulas Formulas
Test for CK+CSO+ID: NESCOND vs KLMLEan Prolog code

Copyright 2013 Nicola Olivetti, Gian Luca Pozzato. NESCOND 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 3 of the License, or (at your option) any later version. NESCOND 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 NESCOND. If not, see http://www.gnu.org/licenses/.