Package com.logic.api

Interface INDProof

public interface INDProof

The INDProof interface represents a natural deduction (ND) proof.

This interface provides methods to access key properties of an ND proof, including:

• Retrieving the conclusion of the proof.
• Iterating over its premises.
• Measuring the height (depth) of the proof tree.
• Determining the total number of steps (size) in the proof.
• Checking whether a given set of premises can derive a specific conclusion.

An implementation of this interface should ensure that the proof structure follows the rules of natural deduction and maintains logical validity.

Since:

04-07-2025

Method Summary

Modifier and Type	Method	Description
com.logic.nd.asts.IASTND	getAST()	Returns the abstract syntax tree (AST) representation of the natural deduction proof.
IFormula	getConclusion()	Retrieves the conclusion of this natural deduction proof.
Iterator<Map.Entry<String,IFormula>>	getHypotheses()	Returns an iterator over the hypotheses used in this proof.
Iterator<IFormula>	getPremises()	Returns an iterator over the premises of this proof.
int	height()	Computes the height (depth) of the proof tree.
int	size()	Computes the total number of steps (nodes) in the proof.

Method Details

getConclusion

IFormula getConclusion()

Retrieves the conclusion of this natural deduction proof.

Returns:

The IFormula representing the final conclusion of the proof.

getHypotheses

Iterator<Map.Entry<String,IFormula>> getHypotheses()

Returns an iterator over the hypotheses used in this proof.

Hypotheses represent assumptions or temporarily introduced formulas during the proof.

Returns:

An Iterator over entries mapping hypothesis labels to their IFormula objects.

getPremises

Iterator<IFormula> getPremises()

Returns an iterator over the premises of this proof.

Premises are the initial assumptions or given statements used in the derivation.

Returns:

An Iterator over the IFormula premises of the proof.

height

int height()

Computes the height (depth) of the proof tree.

The height is the longest path from the root (conclusion) to a leaf (premise).

Returns:

An integer representing the depth of the proof.

size

int size()

Computes the total number of steps (nodes) in the proof.

The size represents the number of inference steps in the proof, including premises and derived formulas.

Returns:

An integer representing the total number of steps in the proof.

getAST

com.logic.nd.asts.IASTND getAST()

Returns the abstract syntax tree (AST) representation of the natural deduction proof.

Returns:

The IASTND object representing the proof's AST.