FCube-4.1 for Intuitionistic Propositional Logic
1. FCube-4.1 verbose version
- This is version 4.1 of FCube-verbose for Tau Prolog (see this discussion), a prover which provides proofs for intuitionistically valid formulas, and countermodels for those that are intuitionistically unprovable.
- I changed the code to use infix notation.
A - Prolog Code:
D - Examples of Queries:
- Excluded Middle: a | ~ a
- Dilemma : ((~ a => b) & (a => b)) => b
- Double Negation: ~(~a) <=> a
- Peirce’s Law: (((a => b) => a) => a)
- Dummett Formula : (a => b)| (b => a)
- Classical equivalence for negation : (~a => a) <=> a
- Classical De Morgan's Law : ~((a & b)) => (~ a | ~b)
- Pelletier Problem 17 : ( ( ( p & ( q => r ) ) => s ) <=> ( ( ~ p | q | s ) & ( ~ p | ~ r | s ) ) )
- a => b
- (a | b) => (a & b)