Assertion Proofs

Assertion proofs are a kind of proof structured in a manner where one starts with a set of statements they would like to prove in terms of another set of statements. Deductive makes this distinction so that a given-goal structure can be defined which describes such a system.

Given Goal Proofs

Given-goal systems are useful for a number of reasons, such as allowing for clear meta-transformations like a contradictory or contrapositive system, better reflecting the underlying form which mathematical proofs usually fall under, and cutting down on search algorithm costs by utilizing inference rules as a means of statement transformation instead of replacement rules, which can be applied recursively to an expression tree rather than just the "top".

Deductive.GivenGoal — Type

GivenGoal(given::Set{AbstractExpression}, goal::Set{AbstractExpression})

Initialize a structure representing a proof starting and ending point, with given and goal sets of expressions respectively. This structure on its own isn't enough to conduct a proof, however. A proof requires both a GivenGoal and a logical calculus which defines the allowed elementary operations on expressions. For example, if operating within propositional logic, see the PropositionalCalculus definition.

source

Deductive.given — Function

given(gg::GivenGoal)

Returns the given part of a GivenGoal

source

Deductive.goal — Function

goal(gg::GivenGoal)

Returns the goal part of a GivenGoal

source

Matching Algorithms

The given-goal proof definition requires one to apply inference rules repeatedly. These inference rules take the form of a set of expressions which, when matched to a subset of the statements in a given section of a proof, the conclusion part of the inference rule becomes the logical consequence of that subset of given statements.

Deductive.rule_matches — Function

rule_matches(ir::InferenceRule, haystack::Set{T}) where {T <: AbstractExpression}

Computes a vector of matches in which each element is a valid set of possible symbol values, with the catch being that any two sets drawn from different elements of the output vector may or may not be compatible. It is not recommended that this function be used externally. Instead, see rule_combinations, which outputs a more usable form of rule match, which instead enumerates over all possible matches. Although informationally identical, rule_combinations is usually preferable due to its linearly iterable ouptut.

source

Deductive.rule_combinations — Function

rule_combinations(rule_variables::Set{LogicalSymbol}, reduced_symbol_maps::Vector{Set{SymbolMap}}, current_symbol_map=SymbolMap())

Given a set of variables which all valid combinations must map to and a list of symbol map sets, compute the set of valid combinations of these symbol maps. In most cases this signature should be avoided in favor of the rule_combinations implementation which directly takes an inference rule and set of expressions.

source

rule_combinations(ir::InferenceRule, haystack::Set{T}) where {T <: AbstractExpression}

Find all valid symbol substitutions which can be performed on a set of statements by an inference rule.

Examples

The following code demonstrates that modus ponens can be applied on this set of statements by taking a → b to be true and uses this to imply c. Since the rule for modus ponens is stated with the inference rule (p, p → q) ⊢ q, the variable substitutions corresponding to the logic above would be p => a → b and q => c.

@symbols a b c
modus_ponens = rule_by_name(PropositionalCalculus, "Modus Ponens")
my_premises = Set{AbstractExpression}([
    a → b,
    (a → b) → c
])

rule_combinations(modus_ponens, my_premises)
#= Results in:
Set with 1 element:
  Dict(q => c, p => a → b)
=#

Similarly we inspect an example where multiple possible variable substitutions exist. The rule for double negation introduction is defined as p ⊢ ¬¬p, which can apply universally to all statements in a set of premises.

@symbols a b
double_negation = rule_by_name(PropositionalCalculus, "Double Negation Introduction")
my_premises = Set{AbstractExpression}([
    a,
    b,
    a ∧ b
])

rule_combinations(double_negation, my_premises)
#= Results in:
Set with 3 elements:
  Dict(p => a ∧ b)
  Dict(p => a)
  Dict(p => b)
=#

source

Deductive.is_partner_map — Function

is_partner_map(sym_map::SymbolMap, compare_sym_map::SymbolMap)

Checks whether sym_map and compare_sym_map are "partner maps". Two symbol maps are partners if they do not form any contradictions between their intersection.

source

Deductive.has_partner_map — Function

has_partner_map(sym_map::SymbolMap, compare_sym_map_set::Set{SymbolMap})

Checks whether sym_map has a single partner in the set compare_sym_map_set.

source