Implementing Rules

Implementing a New Rule

This page aims to be a straightforward guide for developers in creating a new rule for Aris. In this example, we will create ∧ Introduction, a fundamental prepositional inference rule used in logic.

Table of Contents

• Step 1: Locate the rule.rs File
• Step 2: Declare the Rule in declare_rules!
• Step 3: Implement Rule Behavior in impl RuleT

Step 1: Locate the rules.rs File

Start by navigating to the rules.rs file in the aris/src directory. Inside this file, you'll find several enums representing various rule categories, such as:

• Propositional Inference Rules
• Predicate Inference Rules
• Boolean Inference Rules
• ...

Since ∧ Introduction is a propositional inference rule, it should be added under the PropositionalInference enum. Update the enum by including the new rule:

#[allow(missing_docs)]
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum PrepositionalInference {
    AndIntro,
    AndElim,
    // Add more rules here
}

Step 2: Declare the Rule in declare_rules!

Scroll down to the declare_rules! section of the file, where each rule is paired with its corresponding SharedChecks(...) declaration. This declaration specifics the checks and logic applied to each rule. For propositional inference rules like ∧ Introduction, the rule is defined with a single Inl wrapper. Add the following line to declare the rule:

        [AndIntro, "CONJUNCTION", (SharedChecks(Inl(PrepositionalInference::AndIntro)))],

Adding Rules to Other Enums

If you're adding a rule to a different enum, such as PredicateInference, you'll need to incrementally nest the Inr wrapper for each additional level. For example:

        [ForallIntro, "UNIVERSAL_GENERALIZATION", (SharedChecks(Inr(Inl(PredicateInference::ForallIntro))))],

For enums beyond PredicateInference, the pattern continues with additional Inr wrappers:

        [SomeRule, "RULE_DESCRIPTION", (SharedChecks(Inr(Inr(Inl(...)))))]

Step 3: Implement Rule Behavior in impl RuleT

Each rule must implement its behavior within the RuleT trait for its enum. For ∧ Introduction, all code is located inside impl RuleT for PropositionalInference. Add logic to the following methods:

get_name

Define the name of the rule as it will appear in the application. For ∧ Introduction:

fn get_name(&self) -> String {
    use PropositionalInference::*;
    match self {
        AndIntro => "∧ Introduction",
        AndElim => "∧ Elimination",
        // Other rules...
    }
    .into()
}

get_classification

Classify the rule as an introduction or elimination:

fn get_classifications(&self) -> HashSet<RuleClassification> {
    use PropositionalInference::*;
    use RuleClassification::*;
    let mut ret = HashSet::new();
    match self {
        AndIntro => {
            ret.insert(Introduction);
        }
        AndElim => {
            ret.insert(Elimination);
        }
        // Other rules...
    }
    ret
}

num_subdeps

Define how many dependencies the rule requires. For ∧ Introduction, this can vary:

fn num_deps(&self) -> Option<usize> {
    use PropositionalInference::*;
    match self {
        AndIntro => None, // Arbitrarily many conjuncts in one application
        AndElim => Some(1),
        // Other rules...
    }
}

num_subdeps

Define the number of subdependencies required:

 fn num_subdeps(&self) -> Option<usize> {
    use PropositionalInference::*;
    match self {
        AndIntro => Some(0),
        AndElim => Some(0),
        // Other rules...
    }
}

check

Implement the logic for verifying the correctness of the rule's application. For ∧ Introduction, ensure:

• Each dependency corresponds to a conjunct in the conclusion.
• Each conjunct in the conclusion has a corresponding dependency.

fn check<P: Proof>(
    self,
    p: &P,
    conclusion: Expr,
    deps: Vec<PjRef<P>>,
    sdeps: Vec<P::SubproofReference>,
) -> Result<(), ProofCheckError<PjRef<P>, P::SubproofReference>> {
    use PropositionalInference::*;
    use ProofCheckError::*;

    match self {
        AndIntro => {
            if let Expr::Assoc { op: Op::And, ref exprs } = conclusion {
                for d in deps.iter() {
                    let e = p.lookup_expr_or_die(d)?;
                    if !exprs.iter().any(|x| x == &e) {
                        return Err(DoesNotOccur(e, conclusion.clone()));
                    }
                }
                for e in exprs {
                    if !deps.iter().any(|d| p.lookup_expr(d).map(|de| &de == e).unwrap_or(false)) {
                        return Err(DepDoesNotExist(e.clone(), false));
                    }
                }
                Ok(())
            } else {
                Err(ConclusionOfWrongForm(Expr::assoc_place_holder(Op::And)))
            }
        }
        _ => unimplemented!(),
    }
}

Congratulations, you've added a rule to Aris! Your next step is to implement testing for the new rule.

Next Steps

This tutorial was intended to give a simple overview of the anatomy of a puzzle in Aris. However, this will (hopefully) have given the reader enough information to be able to read and navigate the source code independently, where the wealth of examples and comments will help to explain the minutia of rules and the application in general.