Index _ | A | B | C | D | E | F | G | H | I | K | L | M | N | O | P | Q | R | S | T | U | V | W | X _ __init__() (unicode_fol_kit.MSFLParser method) (unicode_fol_kit.Node method) A ABox (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.tableau) abox_consistent() (in module unicode_fol_kit.dl) (in module unicode_fol_kit.dl.tableau) add() (unicode_fol_kit.dl.tableau.TBox method) (unicode_fol_kit.dl.TBox method) add_equivalence() (unicode_fol_kit.dl.tableau.TBox method) (unicode_fol_kit.dl.TBox method) And (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) announce() (in module unicode_fol_kit) (in module unicode_fol_kit.semantics.dynamic_epistemic) apply_subst() (in module unicode_fol_kit) assert_concept() (unicode_fol_kit.dl.ABox method) (unicode_fol_kit.dl.tableau.ABox method) assert_role() (unicode_fol_kit.dl.ABox method) (unicode_fol_kit.dl.tableau.ABox method) Atomic (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) atoms() (unicode_fol_kit.Node method) B beta_eta_normalize() (in module unicode_fol_kit) Bottom (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) box_announce() (in module unicode_fol_kit.semantics.dynamic_epistemic) BuildResult (class in unicode_fol_kit.hol.isabelle_runner) C check_ill_proof() (in module unicode_fol_kit) check_lambek_proof() (in module unicode_fol_kit) check_lj_proof() (in module unicode_fol_kit) check_logical_entailment() (in module unicode_fol_kit) check_logical_entailment_vampire() (in module unicode_fol_kit) check_proof() (in module unicode_fol_kit) check_sequent_proof() (in module unicode_fol_kit) check_theory() (in module unicode_fol_kit.hol.isabelle_runner) Concept (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) concept (unicode_fol_kit.dl.concepts.Exists attribute) (unicode_fol_kit.dl.concepts.ForAll attribute) (unicode_fol_kit.dl.concepts.Not attribute) (unicode_fol_kit.dl.Exists attribute) (unicode_fol_kit.dl.ForAll attribute) (unicode_fol_kit.dl.Not attribute) concept_assertions (unicode_fol_kit.dl.ABox attribute) (unicode_fol_kit.dl.tableau.ABox attribute) concept_satisfiable() (in module unicode_fol_kit.dl) (in module unicode_fol_kit.dl.tableau) concept_unsatisfiable() (in module unicode_fol_kit.dl) (in module unicode_fol_kit.dl.tableau) conditional_faithfulness_theory() (in module unicode_fol_kit) conj (unicode_fol_kit.semantics.matrix.TruthMatrix attribute) (unicode_fol_kit.semantics.tnorm.TNorm attribute) constants (unicode_fol_kit.semantics.free_logic.FreeModel attribute) count() (unicode_fol_kit.Node method) CounterfactualModel (class in unicode_fol_kit.semantics.conditional) countermodel (unicode_fol_kit.hol.isabelle_runner.FolVerdict attribute) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) cygwin_bash (unicode_fol_kit.hol.isabelle_runner.IsabelleInstall attribute) D depth() (unicode_fol_kit.Node method) designated (unicode_fol_kit.semantics.matrix.TruthMatrix attribute) diamond_announce() (in module unicode_fol_kit.semantics.dynamic_epistemic) disj (unicode_fol_kit.semantics.matrix.TruthMatrix attribute) (unicode_fol_kit.semantics.tnorm.TNorm attribute) E elapsed (unicode_fol_kit.hol.isabelle_runner.BuildResult attribute) eliminate_lambdas() (in module unicode_fol_kit) equiv() (unicode_fol_kit.semantics.tnorm.TNorm method) equivalent() (in module unicode_fol_kit.dl) (in module unicode_fol_kit.dl.tableau) existing (unicode_fol_kit.semantics.free_logic.FreeModel attribute) Exists (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) exit_code (unicode_fol_kit.hol.isabelle_runner.BuildResult attribute) F find_countermodel() (in module unicode_fol_kit) find_fitch_proof() (in module unicode_fol_kit) find_isabelle() (in module unicode_fol_kit.hol.isabelle_runner) find_model() (in module unicode_fol_kit) FolVerdict (class in unicode_fol_kit.hol.isabelle_runner) ForAll (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) formulas_are_equivalent() (in module unicode_fol_kit) frame (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) free_holds() (in module unicode_fol_kit) (in module unicode_fol_kit.semantics.free_logic) free_satisfies() (in module unicode_fol_kit.semantics.free_logic) free_variables() (in module unicode_fol_kit) FreeModel (class in unicode_fol_kit.semantics.free_logic) from_dict() (unicode_fol_kit.Node static method) from_functions() (unicode_fol_kit.semantics.matrix.TruthMatrix static method) from_z3() (in module unicode_fol_kit) functions (unicode_fol_kit.semantics.free_logic.FreeModel attribute) fuzzy_evaluate() (in module unicode_fol_kit) fuzzy_is_valid() (in module unicode_fol_kit) G get_model() (in module unicode_fol_kit) get_tnorm() (in module unicode_fol_kit) (in module unicode_fol_kit.semantics.tnorm) H has_modal() (in module unicode_fol_kit.atp.modal_tableau) home (unicode_fol_kit.hol.isabelle_runner.IsabelleInstall attribute) hybrid_is_valid() (in module unicode_fol_kit) I iff (unicode_fol_kit.semantics.matrix.TruthMatrix attribute) ill_derivable() (in module unicode_fol_kit) ill_prove() (in module unicode_fol_kit) impl (unicode_fol_kit.semantics.matrix.TruthMatrix attribute) (unicode_fol_kit.semantics.tnorm.TNorm attribute) inclusions (unicode_fol_kit.dl.tableau.TBox attribute) (unicode_fol_kit.dl.TBox attribute) infra_error (unicode_fol_kit.hol.isabelle_runner.FolVerdict attribute) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) int_countermodel() (in module unicode_fol_kit) int_valid() (in module unicode_fol_kit) internalized() (unicode_fol_kit.dl.tableau.TBox method) (unicode_fol_kit.dl.TBox method) intuitionistic_faithfulness_theory() (in module unicode_fol_kit) is_designated() (unicode_fol_kit.semantics.matrix.TruthMatrix method) is_horn() (in module unicode_fol_kit) is_invalid (unicode_fol_kit.hol.isabelle_runner.FolVerdict property) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict property) is_modal_valid() (in module unicode_fol_kit) (in module unicode_fol_kit.atp.modal_tableau) is_satisfiable() (in module unicode_fol_kit) is_satisfiable_arith() (in module unicode_fol_kit) is_satisfiable_finite() (in module unicode_fol_kit) is_unknown (unicode_fol_kit.hol.isabelle_runner.FolVerdict property) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict property) is_valid (unicode_fol_kit.hol.isabelle_runner.FolVerdict property) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict property) is_valid() (in module unicode_fol_kit) is_valid_arith() (in module unicode_fol_kit) is_valid_finite() (in module unicode_fol_kit) is_valid_fitch() (in module unicode_fol_kit) is_valid_resolution() (in module unicode_fol_kit) is_valid_tableau() (in module unicode_fol_kit) is_windows (unicode_fol_kit.hol.isabelle_runner.IsabelleInstall attribute) isabelle_available() (in module unicode_fol_kit.hol.isabelle_runner) isabelle_decide_fol() (in module unicode_fol_kit) (in module unicode_fol_kit.hol.isabelle_runner) isabelle_decide_modal() (in module unicode_fol_kit) (in module unicode_fol_kit.hol.isabelle_runner) isabelle_exe (unicode_fol_kit.hol.isabelle_runner.IsabelleInstall attribute) IsabelleInstall (class in unicode_fol_kit.hol.isabelle_runner) IsabelleNotAvailable K kleene_value() (in module unicode_fol_kit) L lambek_derivable() (in module unicode_fol_kit) lambek_prove() (in module unicode_fol_kit) latex_to_unicode() (in module unicode_fol_kit) left (unicode_fol_kit.dl.And attribute) (unicode_fol_kit.dl.concepts.And attribute) (unicode_fol_kit.dl.concepts.Or attribute) (unicode_fol_kit.dl.Or attribute) load_prover9() (in module unicode_fol_kit) load_smtlib() (in module unicode_fol_kit) load_tptp() (in module unicode_fol_kit) M map_children() (unicode_fol_kit.Node method) matrix_entails() (in module unicode_fol_kit) (in module unicode_fol_kit.semantics.matrix) matrix_is_satisfiable() (in module unicode_fol_kit.semantics.matrix) matrix_is_valid() (in module unicode_fol_kit) (in module unicode_fol_kit.semantics.matrix) matrix_value() (in module unicode_fol_kit.semantics.matrix) method (unicode_fol_kit.hol.isabelle_runner.FolVerdict attribute) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) might() (in module unicode_fol_kit.semantics.conditional) minimal_entails() (in module unicode_fol_kit) (in module unicode_fol_kit.semantics.nonmonotonic) minimal_models() (in module unicode_fol_kit.semantics.nonmonotonic) modal_countermodel() (in module unicode_fol_kit) (in module unicode_fol_kit.atp.modal_tableau) modal_decide() (in module unicode_fol_kit) (in module unicode_fol_kit.atp.modal_tableau) modal_faithfulness_theory() (in module unicode_fol_kit) modal_prove() (in module unicode_fol_kit) (in module unicode_fol_kit.atp.modal_tableau) modal_tableau_closed() (in module unicode_fol_kit.atp.modal_tableau) ModalVerdict (class in unicode_fol_kit.hol.isabelle_runner) mode (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) module unicode_fol_kit.atp.modal_tableau unicode_fol_kit.dl unicode_fol_kit.dl.concepts unicode_fol_kit.dl.tableau unicode_fol_kit.hol.isabelle_runner unicode_fol_kit.semantics.conditional unicode_fol_kit.semantics.dynamic_epistemic unicode_fol_kit.semantics.free_logic unicode_fol_kit.semantics.matrix unicode_fol_kit.semantics.nonmonotonic unicode_fol_kit.semantics.tnorm MSFLParser (class in unicode_fol_kit) N name (unicode_fol_kit.dl.Atomic attribute) (unicode_fol_kit.dl.concepts.Atomic attribute) (unicode_fol_kit.semantics.matrix.TruthMatrix attribute) (unicode_fol_kit.semantics.tnorm.TNorm attribute) neg (unicode_fol_kit.semantics.matrix.TruthMatrix attribute) (unicode_fol_kit.semantics.tnorm.TNorm attribute) nnf() (in module unicode_fol_kit.dl) (in module unicode_fol_kit.dl.concepts) Node (class in unicode_fol_kit) Not (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) O ok (unicode_fol_kit.hol.isabelle_runner.BuildResult attribute) Or (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) outer (unicode_fol_kit.semantics.free_logic.FreeModel attribute) output (unicode_fol_kit.hol.isabelle_runner.BuildResult attribute) P parse() (unicode_fol_kit.MSFLParser method) parse_latex() (in module unicode_fol_kit) parse_prover9() (in module unicode_fol_kit) parse_prover9_problem() (in module unicode_fol_kit) parse_smtlib() (in module unicode_fol_kit) parse_tptp() (in module unicode_fol_kit) parse_tptp_formula() (in module unicode_fol_kit) predicates (unicode_fol_kit.semantics.free_logic.FreeModel attribute) prove() (in module unicode_fol_kit) prove_elapsed (unicode_fol_kit.hol.isabelle_runner.FolVerdict attribute) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) prove_output (unicode_fol_kit.hol.isabelle_runner.FolVerdict attribute) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) prove_tableau() (in module unicode_fol_kit) Q qml_equivalent() (in module unicode_fol_kit) qml_is_valid() (in module unicode_fol_kit) R reduce_trace() (in module unicode_fol_kit) refute_elapsed (unicode_fol_kit.hol.isabelle_runner.FolVerdict attribute) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) refute_output (unicode_fol_kit.hol.isabelle_runner.FolVerdict attribute) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) rel_countermodel() (in module unicode_fol_kit) rel_satisfies() (in module unicode_fol_kit) rel_valid() (in module unicode_fol_kit) relevant_faithfulness_theory() (in module unicode_fol_kit) render_fitch() (in module unicode_fol_kit) right (unicode_fol_kit.dl.And attribute) (unicode_fol_kit.dl.concepts.And attribute) (unicode_fol_kit.dl.concepts.Or attribute) (unicode_fol_kit.dl.Or attribute) role (unicode_fol_kit.dl.concepts.Exists attribute) (unicode_fol_kit.dl.concepts.ForAll attribute) (unicode_fol_kit.dl.Exists attribute) (unicode_fol_kit.dl.ForAll attribute) role_assertions (unicode_fol_kit.dl.ABox attribute) (unicode_fol_kit.dl.tableau.ABox attribute) S sanitize_all() (in module unicode_fol_kit) sanitize_names() (in module unicode_fol_kit) satisfies_modal() (in module unicode_fol_kit) satisfies_so() (in module unicode_fol_kit) session (unicode_fol_kit.hol.isabelle_runner.BuildResult attribute) skolemize() (in module unicode_fol_kit) so_find_countermodel() (in module unicode_fol_kit) so_is_valid_finite() (in module unicode_fol_kit) sphere_system() (unicode_fol_kit.semantics.conditional.CounterfactualModel method) spheres (unicode_fol_kit.semantics.conditional.CounterfactualModel attribute) standard_translation() (in module unicode_fol_kit) status (unicode_fol_kit.hol.isabelle_runner.FolVerdict attribute) (unicode_fol_kit.hol.isabelle_runner.ModalVerdict attribute) subformulas() (unicode_fol_kit.Node method) substitute() (in module unicode_fol_kit) subsumes() (in module unicode_fol_kit.dl) (in module unicode_fol_kit.dl.tableau) T tableau_model() (in module unicode_fol_kit) TBox (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.tableau) team_models() (in module unicode_fol_kit) team_satisfies() (in module unicode_fol_kit) theory_name (unicode_fol_kit.hol.isabelle_runner.BuildResult attribute) TNorm (class in unicode_fol_kit.semantics.tnorm) to_cnf() (in module unicode_fol_kit) to_dict() (unicode_fol_kit.Node method) to_dnf() (in module unicode_fol_kit) to_dot() (unicode_fol_kit.Node method) to_english() (in module unicode_fol_kit) to_fol() (in module unicode_fol_kit) to_isabelle_modal() (in module unicode_fol_kit) to_latex() (unicode_fol_kit.Node method) to_msfol() (unicode_fol_kit.Node method) to_nnf() (in module unicode_fol_kit) to_pnf() (in module unicode_fol_kit) to_prover9() (unicode_fol_kit.Node method) to_thf_modal() (in module unicode_fol_kit) to_tptp() (unicode_fol_kit.Node method) to_tseitin_cnf() (in module unicode_fol_kit) to_unicode() (unicode_fol_kit.dl.Concept method) (unicode_fol_kit.dl.concepts.Concept method) to_unicode_str() (unicode_fol_kit.Node method) to_z3() (unicode_fol_kit.Node method) Top (class in unicode_fol_kit.dl) (class in unicode_fol_kit.dl.concepts) tree_str() (unicode_fol_kit.Node method) truth_table() (in module unicode_fol_kit) TruthMatrix (class in unicode_fol_kit.semantics.matrix) U unicode_fol_kit.atp.modal_tableau module unicode_fol_kit.dl module unicode_fol_kit.dl.concepts module unicode_fol_kit.dl.tableau module unicode_fol_kit.hol.isabelle_runner module unicode_fol_kit.semantics.conditional module unicode_fol_kit.semantics.dynamic_epistemic module unicode_fol_kit.semantics.free_logic module unicode_fol_kit.semantics.matrix module unicode_fol_kit.semantics.nonmonotonic module unicode_fol_kit.semantics.tnorm module unify() (in module unicode_fol_kit) V valuation (unicode_fol_kit.semantics.conditional.CounterfactualModel attribute) values (unicode_fol_kit.semantics.matrix.TruthMatrix attribute) variables() (unicode_fol_kit.Node method) version (unicode_fol_kit.hol.isabelle_runner.IsabelleInstall attribute) W walk() (unicode_fol_kit.Node method) worlds (unicode_fol_kit.semantics.conditional.CounterfactualModel attribute) would() (in module unicode_fol_kit) (in module unicode_fol_kit.semantics.conditional) X xor (unicode_fol_kit.semantics.matrix.TruthMatrix attribute)