Index

_

__eq__() (predicates.proofs.Schema method) (predicates.syntax.Formula method) (predicates.syntax.Term method) (propositions.proofs.InferenceRule method) (propositions.syntax.Formula method) __init__() (predicates.proofs.Proof method) (predicates.proofs.Proof.AssumptionLine method) (predicates.proofs.Proof.MPLine method) (predicates.proofs.Proof.TautologyLine method) (predicates.proofs.Proof.UGLine method) (predicates.proofs.Schema method) (predicates.proofs.Schema.BoundVariableError method) (predicates.prover.Prover method) (predicates.semantics.Model method) (predicates.syntax.ForbiddenVariableError method) (predicates.syntax.Formula method) (predicates.syntax.Term method) (propositions.proofs.InferenceRule method) (propositions.proofs.Proof method) (propositions.proofs.Proof.Line method) (propositions.syntax.Formula method) __ne__() (predicates.proofs.Schema method) (predicates.syntax.Formula method) (predicates.syntax.Term method) (propositions.proofs.InferenceRule method) (propositions.syntax.Formula method) __repr__() (predicates.proofs.Proof method) (predicates.proofs.Proof.AssumptionLine method) (predicates.proofs.Proof.MPLine method) (predicates.proofs.Proof.TautologyLine method) (predicates.proofs.Proof.UGLine method) (predicates.proofs.Schema method) (predicates.semantics.Model method) (predicates.syntax.Formula method) (predicates.syntax.Term method) (propositions.proofs.InferenceRule method) (propositions.proofs.Proof method) (propositions.proofs.Proof.Line method) (propositions.syntax.Formula method)

_add_chaining_of_two_equalities() (predicates.prover.Prover method) _add_line() (predicates.prover.Prover method) _axiom_specialization_map_to_schema_instantiation_map() (in module predicates.proofs) _CM (in module propositions.some_proofs) _compile_term() (in module predicates.functions) _CP (in module propositions.some_proofs) _formula_specialization_map() (propositions.proofs.InferenceRule static method) _inline_proof_once() (in module propositions.proofs) _instantiate_helper() (predicates.proofs.Schema static method) _merge_specialization_maps() (propositions.proofs.InferenceRule static method) _NNE (in module propositions.some_proofs) _parse_prefix() (predicates.syntax.Formula static method) (predicates.syntax.Term static method) (propositions.syntax.Formula static method) _prove_CM() (in module propositions.some_proofs) _prove_CP() (in module propositions.some_proofs) _prove_exists_not_implies_not_all() (in module predicates.some_proofs) _prove_from_skeleton_proof() (in module predicates.proofs) _prove_NNE() (in module propositions.some_proofs) _prove_not_exists_not_implies_all() (in module predicates.some_proofs) _pull_out_quantifications_across_binary_operator() (in module predicates.prenex) _pull_out_quantifications_across_negation() (in module predicates.prenex) _pull_out_quantifications_from_left_across_binary_operator() (in module predicates.prenex) _pull_out_quantifications_from_right_across_binary_operator() (in module predicates.prenex) _synthesize_for_all_except_model() (in module propositions.semantics) _synthesize_for_model() (in module propositions.semantics) _to_prenex_normal_form_from_uniquely_named_variables() (in module predicates.prenex) _uniquely_rename_quantified_variables() (in module predicates.prenex)

A

A (in module propositions.axiomatic_systems) A_RULE (in module propositions.some_proofs) add_assumption() (predicates.prover.Prover method) add_chained_equality() (predicates.prover.Prover method) add_existential_derivation() (predicates.prover.Prover method) add_flipped_equality() (predicates.prover.Prover method) add_free_instantiation() (predicates.prover.Prover method) add_instantiated_assumption() (predicates.prover.Prover method) add_mp() (predicates.prover.Prover method) add_proof() (predicates.prover.Prover method) add_SAME_as_equality_in_model() (in module predicates.functions) add_substituted_equality() (predicates.prover.Prover method) add_tautological_implication() (predicates.prover.Prover method)

add_tautology() (predicates.prover.Prover method) add_ug() (predicates.prover.Prover method) add_universal_instantiation() (predicates.prover.Prover method) ADDITIONAL_QUANTIFICATION_AXIOMS (in module predicates.prenex) AE1 (in module propositions.axiomatic_systems) AE1_RULE (in module propositions.some_proofs) AE2 (in module propositions.axiomatic_systems) AE2_RULE (in module propositions.some_proofs) all_models() (in module propositions.semantics) assignment_to_3coloring() (in module propositions.reductions) AXIOMATIC_SYSTEM (in module propositions.axiomatic_systems) AXIOMATIC_SYSTEM_FULL (in module propositions.axiomatic_systems) AXIOMS (predicates.prover.Prover attribute)

C

combine_contradictions() (in module predicates.completeness) combine_proofs() (in module propositions.deduction)

COMPREHENSION_AXIOM (in module predicates.some_proofs) constants() (predicates.syntax.Formula method) (predicates.syntax.Term method)

D

D (in module propositions.axiomatic_systems)

D_SCHEMA (in module predicates.proofs)

E

EI (predicates.prover.Prover attribute) eliminate_existential_witness_assumption() (in module predicates.completeness) eliminate_universal_instantiation_assumption() (in module predicates.completeness) encode_as_formula() (in module propositions.tautology) equivalence_of() (in module predicates.prenex)

ES (predicates.prover.Prover attribute) evaluate() (in module propositions.semantics) evaluate_formula() (predicates.semantics.Model method) evaluate_inference() (in module propositions.semantics) evaluate_term() (predicates.semantics.Model method) existential_closure_step() (in module predicates.completeness)

F

FIELD_AXIOMS (in module predicates.some_proofs) find_unsatisfied_quantifier_free_sentence() (in module predicates.completeness) ForbiddenVariableError Formula (class in predicates.syntax) (class in propositions.syntax) formulas_capturing_model() (in module propositions.tautology) free_variables() (predicates.syntax.Formula method)

fresh_constant_name_generator (in module logic_utils) fresh_variable_name_generator (in module logic_utils) from_propositional_skeleton() (predicates.syntax.Formula static method) frozen() (in module logic_utils) frozendict (class in logic_utils) function_name_to_relation_name() (in module predicates.functions) functions() (predicates.syntax.Formula method) (predicates.syntax.Term method)

G

get_constants() (in module predicates.completeness) get_primitives() (in module predicates.completeness)

Graph (in module propositions.reductions) graph3coloring_to_formula() (in module propositions.reductions) GROUP_AXIOMS (in module predicates.some_proofs)

H

half() (in module prelim.prelim) has_uniquely_named_variables() (in module predicates.prenex) HILBERT_AXIOMATIC_SYSTEM (in module propositions.axiomatic_systems)

HILBERT_AXIOMATIC_SYSTEM_ALTERNATIVE (in module propositions.axiomatic_systems) HILBERT_AXIOMATIC_SYSTEM_FULL (in module propositions.axiomatic_systems) HS (in module propositions.some_proofs)

I

I0 (in module propositions.axiomatic_systems) I0_SCHEMA (in module predicates.proofs) I1 (in module propositions.axiomatic_systems) I1_SCHEMA (in module predicates.proofs) I2 (in module propositions.axiomatic_systems) I2_SCHEMA (in module predicates.proofs) INDUCTION_AXIOM (in module predicates.some_proofs) InferenceRule (class in propositions.proofs) inline_proof() (in module propositions.proofs) instantiate() (predicates.proofs.Schema method) InstantiationMap (in module predicates.proofs) is_assumption() (propositions.proofs.Proof.Line method) is_binary() (in module predicates.syntax) (in module propositions.syntax) is_closed() (in module predicates.completeness) is_constant() (in module predicates.syntax) (in module propositions.syntax) is_contradiction() (in module propositions.semantics) is_equality() (in module predicates.syntax) is_existentially_closed() (in module predicates.completeness) is_formula() (propositions.syntax.Formula static method) is_function() (in module predicates.syntax) is_graph() (in module propositions.reductions) is_in_prenex_normal_form() (in module predicates.prenex)

is_line_valid() (propositions.proofs.Proof method) is_model() (in module propositions.semantics) is_model_of() (predicates.semantics.Model method) is_primitively_closed() (in module predicates.completeness) is_quantifier() (in module predicates.syntax) is_quantifier_free() (in module predicates.prenex) is_relation() (in module predicates.syntax) is_satisfiable() (in module propositions.semantics) is_sound_inference() (in module propositions.semantics) is_specialization_of() (propositions.proofs.InferenceRule method) is_tautology() (in module propositions.semantics) is_unary() (in module predicates.syntax) (in module propositions.syntax) is_universally_closed() (in module predicates.completeness) is_valid() (predicates.proofs.Proof method) (predicates.proofs.Proof.AssumptionLine method) (predicates.proofs.Proof.MPLine method) (predicates.proofs.Proof.TautologyLine method) (predicates.proofs.Proof.UGLine method) (propositions.proofs.Proof method) is_valid_3coloring() (in module propositions.reductions) is_variable() (in module predicates.syntax) (in module propositions.syntax) is_z_and_number() (in module logic_utils)

L

Line (predicates.proofs.Proof attribute)

logic_utils module

M

make_equality_as_SAME_in_model() (in module predicates.functions) ME (predicates.prover.Prover attribute) memoized_parameterless_method() (in module logic_utils) Model (class in predicates.semantics) (in module propositions.semantics) model_or_inconsistency() (in module predicates.completeness) (in module propositions.tautology) module logic_utils predicates.completeness predicates.deduction predicates.functions predicates.prenex predicates.proofs predicates.prover predicates.semantics predicates.some_proofs predicates.syntax prelim.prelim propositions.axiomatic_systems propositions.deduction propositions.operators propositions.proofs propositions.reductions propositions.semantics propositions.some_proofs propositions.soundness propositions.syntax propositions.tautology

MP (in module propositions.axiomatic_systems)

N

N (in module propositions.axiomatic_systems) N_ALTERNATIVE (in module propositions.axiomatic_systems) N_SCHEMA (in module predicates.proofs) NA1 (in module propositions.axiomatic_systems) NA2 (in module propositions.axiomatic_systems)

NF (in module propositions.axiomatic_systems) NI (in module propositions.axiomatic_systems) NI_SCHEMA (in module predicates.proofs) NN (in module propositions.axiomatic_systems) NN_SCHEMA (in module predicates.proofs) nonsound_rule_of_nonsound_proof() (in module propositions.soundness)

O

OE (in module propositions.axiomatic_systems)

operators() (propositions.syntax.Formula method)

P

parse() (predicates.syntax.Formula static method) (predicates.syntax.Term static method) (propositions.syntax.Formula static method) parse_polish() (propositions.syntax.Formula static method) PEANO_AXIOMS (in module predicates.some_proofs) polish() (propositions.syntax.Formula method) predicates.completeness module predicates.deduction module predicates.functions module predicates.prenex module predicates.proofs module predicates.prover module predicates.semantics module predicates.some_proofs module predicates.syntax module prelim.prelim module print_truth_table() (in module propositions.semantics) Proof (class in predicates.proofs) (class in propositions.proofs) Proof.AssumptionLine (class in predicates.proofs) Proof.Line (class in propositions.proofs) Proof.MPLine (class in predicates.proofs) Proof.TautologyLine (class in predicates.proofs) Proof.UGLine (class in predicates.proofs) proof_or_counterexample() (in module propositions.tautology) PROPOSITIONAL_AXIOM_TO_SCHEMA (in module predicates.proofs) PROPOSITIONAL_AXIOMATIC_SYSTEM_SCHEMAS (in module predicates.proofs) propositional_skeleton() (predicates.syntax.Formula method) propositions.axiomatic_systems module propositions.deduction module propositions.operators module propositions.proofs module propositions.reductions module

propositions.semantics module propositions.some_proofs module propositions.soundness module propositions.syntax module propositions.tautology module prove_and_commutativity() (in module propositions.some_proofs) prove_by_way_of_contradiction() (in module predicates.deduction) (in module propositions.deduction) prove_corollary() (in module propositions.deduction) prove_field_zero_multiplication() (in module predicates.some_proofs) prove_from_opposites() (in module propositions.deduction) prove_group_right_neutral() (in module predicates.some_proofs) prove_group_unique_zero() (in module predicates.some_proofs) prove_homework() (in module predicates.some_proofs) prove_hypothetical_syllogism() (in module propositions.some_proofs) prove_I0() (in module propositions.some_proofs) prove_I2() (in module propositions.some_proofs) prove_in_model() (in module propositions.tautology) prove_in_model_full() (in module propositions.tautology) prove_lovers() (in module predicates.some_proofs) prove_N() (in module propositions.some_proofs) prove_NA1() (in module propositions.some_proofs) prove_NA2() (in module propositions.some_proofs) prove_NI() (in module propositions.some_proofs) prove_NN() (in module propositions.some_proofs) prove_NO() (in module propositions.some_proofs) prove_not_all_iff_exists_not() (in module predicates.some_proofs) prove_peano_left_neutral() (in module predicates.some_proofs) prove_R() (in module propositions.some_proofs) prove_russell_paradox() (in module predicates.some_proofs) prove_sound_inference() (in module propositions.tautology) prove_specialization() (in module propositions.proofs) prove_syllogism() (in module predicates.some_proofs) prove_syllogism_all_all() (in module predicates.some_proofs) prove_syllogism_all_all_with_tautological_implication() (in module predicates.some_proofs) prove_syllogism_all_exists() (in module predicates.some_proofs) prove_syllogism_all_exists_with_existential_derivation() (in module predicates.some_proofs) prove_syllogism_with_universal_instantiation() (in module predicates.some_proofs) prove_tautology() (in module predicates.proofs) (in module propositions.tautology) Prover (class in predicates.prover)

Q

qed() (predicates.prover.Prover method)

R

R (in module propositions.axiomatic_systems) R_SCHEMA (in module predicates.proofs) reduce_assumption() (in module propositions.tautology) relation_name_to_function_name() (in module predicates.functions) relations() (predicates.syntax.Formula method) remove_assumption() (in module predicates.deduction) (in module propositions.deduction) replace_constant() (in module predicates.completeness)

replace_equality_with_SAME_in_formulas() (in module predicates.functions) replace_functions_with_relations_in_formula() (in module predicates.functions) replace_functions_with_relations_in_formulas() (in module predicates.functions) replace_functions_with_relations_in_model() (in module predicates.functions) replace_relations_with_functions_in_model() (in module predicates.functions) rule_for_line() (propositions.proofs.Proof method) rule_nonsoundness_from_specialization_nonsoundness() (in module propositions.soundness) RX (predicates.prover.Prover attribute)

S

Schema (class in predicates.proofs) Schema.BoundVariableError specialization_map() (propositions.proofs.InferenceRule method) SpecializationMap (in module propositions.proofs) specialize() (propositions.proofs.InferenceRule method)

substitute() (predicates.syntax.Formula method) (predicates.syntax.Term method) substitute_operators() (propositions.syntax.Formula method) substitute_variables() (propositions.syntax.Formula method) synthesize() (in module propositions.semantics) synthesize_cnf() (in module propositions.semantics)

T

T (in module predicates.semantics) (in module propositions.axiomatic_systems) Term (class in predicates.syntax) to_implies_false() (in module propositions.operators) to_implies_not() (in module propositions.operators)

to_nand() (in module propositions.operators) to_not_and() (in module propositions.operators) to_not_and_or() (in module propositions.operators) to_prenex_normal_form() (in module predicates.prenex) tricolor_graph() (in module propositions.reductions) truth_values() (in module propositions.semantics)

U

UI (predicates.prover.Prover attribute)

universal_closure_step() (in module predicates.completeness) US (predicates.prover.Prover attribute)

V

variables() (in module propositions.semantics) (predicates.syntax.Formula method) (predicates.syntax.Term method) (propositions.proofs.InferenceRule method) (propositions.syntax.Formula method)