Automated Reasoning in Modal Logics
Handout (PDF) - presented in van Benthem's Modal Logic class at Stanford (5/02)
Otter input files (ASCII)
- hilbert_otter.txt - Basic Otter input file for proofs in "normal" modal logics
- interp_otter.txt - Basic Otter input file for proofs in interpretability logics
- kripke.txt - Basic Otter input file for proofs in kripke semantics
Paradox input files (ASCII) -- added 11/04 [makes MACE and MaGIC files obsolete]
- hilbert_paradox.txt - Paradox file for matrices of "normal" modal logics
- interp_paradox.txt - Paradox file for matrices of interpretability logics
- kripke_paradox.txt - Paradox file for kripke models
MACE input files (ASCII)
- hilbert_mace.txt - MACE input file for matrices of "normal" modal logics
- interp_mace.txt - MACE input file for matrices of interpretability logics
- kripke.txt - MACE input file for kripke
models
MaGIC syntax files (ASCII)
- hilbert_magic.txt - MaGIC syntax file for matrices of "normal" modal logics
- interp_magic.txt - MaGIC syntax file for matrices of interpretability logics