Package com.logic.api

Class LogicAPI

java.lang.Object

com.logic.api.LogicAPI

public class LogicAPI
extends Object

The LogicAPI class provides utility methods for parsing and verifying logical expressions and natural deduction proofs. It supports:

• Parsing and checking well-formedness of propositional logic (PL) formulas.
• Parsing and checking well-formedness of first-order logic (FOL) formulas.
• Parsing and validating natural deduction (ND) proofs for both PL and FOL.

This class is not intended to be instantiated.

Since:

08-03-2025

Method Summary

Modifier and Type	Method	Description
static INDProof	checkNDProblem(INDProof proof, Set<IFormula> premises, IFormula conclusion)	Validates a complete natural deduction (ND) proof against a set of premises and an expected conclusion.
static IFOLFormula	parseFOL(String expression)	Parses a first-order logic (FOL) formula and checks if it is well-formed.
static INDProof	parseNDFOLProof(String expression)	Parses and validates a natural deduction (ND) proof for first-order logic (FOL).
static INDProof	parseNDPLProof(String expression)	Parses and validates a natural deduction (ND) proof for propositional logic (PL).
static IPLFormula	parsePL(String expression)	Parses a propositional logic (PL) formula and checks if it is well-formed.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Details

parsePL

public static IPLFormula parsePL(String expression)
                          throws com.logic.exps.exceptions.ExpException

Parses a propositional logic (PL) formula and checks if it is well-formed.

This method takes a propositional logic expression as a string, parses it, and ensures that it is a well-formed formula (WFF) before returning the parsed representation.

Propositional Logic Syntax:

• Literals: Lowercase characters (a-z).
• Generics: φ, δ, ψ, α, β, γ.
• Logical Symbols: ¬ (negation), → (implication), ↔ (biconditional), ∧ (conjunction), ∨ (disjunction), ⊥ (false), ⊤ (true).

Parameters:

expression - The propositional logic formula to parse and check.

Returns:

The parsed IPLFormula representation of the formula.

Throws:

com.logic.exps.exceptions.ExpException - If the formula return an error.

parseFOL

public static IFOLFormula parseFOL(String expression)
                            throws com.logic.exps.exceptions.ExpException

Parses a first-order logic (FOL) formula and checks if it is well-formed.

This method takes a first-order logic expression as a string, parses it, and ensures that it is a well-formed formula (WFF) before returning the parsed representation.

First-Order Logic Syntax:

• Generics: φ, δ, ψ, α, β, γ (optionally followed by a number, e.g., φ1, φ2).
• Logical Symbols: ¬, →, ↔, ∧, ∨, ⊥, ⊤.
• Variables: Lowercase letters (w-z) with optional numbers (e.g., x1, x2).
• Predicates: Uppercase words (e.g., Father(...), Adult(...), L(...), L).
• Functions: Lowercase words (e.g., height(...), weight(...), f(...), daniel).

Parameters:

expression - The first-order logic formula to parse and check.

Returns:

The parsed IFOLFormula representation of the formula.

Throws:

com.logic.exps.exceptions.ExpException - If the formula return an error.

parseNDPLProof

public static INDProof parseNDPLProof(String expression)
                               throws com.logic.exps.exceptions.ExpException,
com.logic.nd.exceptions.NDRuleException

Parses and validates a natural deduction (ND) proof for propositional logic (PL).

This method takes a structured ND proof as a string, parses it, and ensures its correctness by:

• Checking that all expressions in the proof are well-formed formulas (WFFs).
• Validating the correctness of rule applications.
• Ensuring that proof structure follows ND inference rules.

Supported ND Inference Rules:

Each rule is represented in the format: [Rule Name, optional marks] [formula. [rule references]]

• Absurdity (⊥ Introduction): [⊥, m] [formula. [rule]]
• Negation Introduction (¬I): [¬I, m] [formula. [rule]]
• Negation Elimination (¬E): [¬E] [⊥. [rule1] [rule2]]
• Conjunction Elimination Left (∧El): [∧El] [formula. [rule]]
• Conjunction Elimination Right (∧Er): [∧Er] [formula. [rule]]
• Conjunction Introduction (∧I): [∧I] [formula. [rule1] [rule2]]
• Disjunction Introduction Left (∨Il): [∨Il] [formula. [rule]]
• Disjunction Introduction Right (∨Ir): [∨Ir] [formula. [rule]]
• Disjunction Elimination (∨E): [∨E, m, n] [formula. [rule1] [rule2] [rule3]]
• Implication Introduction (→I): [→I, m] [formula. [rule]]
• Implication Elimination (→E): [→E] [formula. [rule1] [rule2]]

Example of a Valid ND Proof:

 [→I, 1] [(p ∨ q) → (q ∨ p).
     [∨E, 2, 3] [q ∨ p.
         [H, 1] [p ∨ q.]
         [∨Il] [q ∨ p.
             [H, 2] [p.]]
         [∨Ir] [q ∨ p.
             [H, 3] [q.]]]]
 

Parameters:

expression - The string representation of the propositional logic ND proof.

Returns:

The parsed and validated INDProof object.

Throws:

com.logic.exps.exceptions.ExpException - If the proof contains an invalid expression.

com.logic.nd.exceptions.NDRuleException - If the proof uses a rule incorrectly.

parseNDFOLProof

public static INDProof parseNDFOLProof(String expression)
                                throws com.logic.exps.exceptions.ExpException,
com.logic.nd.exceptions.NDRuleException

Parses and validates a natural deduction (ND) proof for first-order logic (FOL).

This method takes a structured ND proof as a string, parses it, and ensures its correctness by:

• Checking that all expressions in the proof are well-formed formulas (WFFs).
• Validating the correctness of rule applications.
• Ensuring that proof structure follows ND inference rules.
• Verifying side conditions specific to first-order logic.

Supported ND Inference Rules:

Each rule is represented in the format: [Rule Name, optional marks] [formula. [rule references]]

The following rules are valid in FOL, including all the propositional logic (PL) rules:

• Universal Introduction (∀I): [∀I] [formula. [rule]]
• Universal Elimination (∀E): [∀E] [formula. [rule]]
• Existential Introduction (∃I): [∃I] [formula. [rule]]
• Existential Elimination (∃E): [∃E, m] [formula. [rule1] [rule2]]

Example of a Valid ND Proof:

 [→I, 2] [¬∃x P(x) → ∀x ¬P(x).
     [∀I] [∀x ¬P(x).
         [¬I, 1] [¬P(x).
             [¬E] [⊥.
                 [H, 2] [¬∃x P(x).]
                 [∃I] [∃x P(x).
                     [H, 1] [P(x).]]]]]]
 

Parameters:

expression - The string representation of the first-order logic ND proof.

Returns:

The parsed and validated INDProof object.

Throws:

com.logic.exps.exceptions.ExpException - If the proof contains an invalid expression.

com.logic.nd.exceptions.NDRuleException - If the proof uses a rule incorrectly.

checkNDProblem

public static INDProof checkNDProblem(INDProof proof,
 Set<IFormula> premises,
 IFormula conclusion)
                               throws com.logic.exps.exceptions.ExpException,
com.logic.nd.exceptions.NDRuleException

Validates a complete natural deduction (ND) proof against a set of premises and an expected conclusion.

This method checks whether the given ND proof:

• Is correctly derived using valid ND inference rules.
• Properly uses the provided premises.
• Successfully derives the expected conclusion as the final line of the proof.

Use Case:

This method is ideal for validating that a user's proof actually solves a logical problem (e.g., exercises or automated grading).

Parameters:

proof - The structured and validated ND proof object.

premises - The set of initial premises the proof must be based on.

conclusion - The formula that should be concluded from the premises.

Returns:

The same INDProof object if the proof solves the problem.

Throws:

com.logic.exps.exceptions.ExpException - If any expressions in the proof are invalid.

com.logic.nd.exceptions.NDRuleException - If the proof is structurally incorrect or does not derive the conclusion.