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

CK and basic extensions

System Axiom Prolog
CK - code
ID a => a code
MP (a => b) -> ( a -> b) code
CEM (a => b) v (a => !b) code
CSO ((a => b) ^ (b => a)) -> ((a => c) -> (b => c)) -

Other extensions

System Prolog
CK+ID+MP code
CK+CEM+ID code
CK+CSO+ID (flat fragment) code

Other source files

 Prolog
Definition of connectives 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/.