Package com.logic.api

Interface IFOLFormula

All Superinterfaces:

IFormula

public interface IFOLFormula
extends IFormula

The IFOLFormula interface defines a first-order logic formula. This interface provides methods for iterating over different components of a first-order logic formula, such as functions, predicates, bounded variables, unbounded variables, and terms. It also includes methods for checking whether a variable belongs to a specific category and whether the formula is a sentence. Implementations of IFOLFormula represent logical expressions composed of:

• Functions (e.g., f(x), g(a, b))
• Predicates (e.g., P(x), Parent(x, y))
• Bounded variables (variables within quantifier scopes, e.g., ∀x, ∃y)
• Unbounded (free) variables
• Terms (sub-expressions within a formula)
• Sentences (formulas with no free variables)

This interface allows structured manipulation of logical formulas, supporting operations such as variable classification, expression iteration, and sentence validation.

Since:

08-03-2025

See Also:

• LogicAPI

Method Summary

Modifier and Type	Method	Description
boolean	appearsFreeVariable(com.logic.exps.asts.others.ASTVariable variable)	Determines whether the specified variable is a free variable in this formula.
boolean	isABoundedVariable(com.logic.exps.asts.others.ASTVariable variable)	Determines whether the specified variable is a bounded variable in this formula.
boolean	isAnUnboundedVariable(com.logic.exps.asts.others.ASTVariable variable)	Determines whether the specified variable is an unbounded variable in this formula.
boolean	isASentence()	Checks whether this first-order logic formula is a sentence.
boolean	isAVariable(com.logic.exps.asts.others.ASTVariable variable)	Determines whether the specified variable exists in this formula (either bounded or unbounded).
boolean	isFreeVariable(com.logic.exps.asts.others.ASTVariable variable)	Checks whether a variable is free (not bounded) in the formula.
Iterator<com.logic.exps.asts.others.ASTVariable>	iterateBoundedVariables()	Returns an iterator over all bounded variables in this formula.
Iterator<com.logic.exps.asts.others.ASTFun>	iterateFunctions()	Returns an iterator over all function symbols used in this first-order logic formula.
Iterator<com.logic.exps.asts.others.ASTPred>	iteratePredicates()	Returns an iterator over all predicate symbols used in this first-order logic formula.
Iterator<com.logic.exps.asts.others.AASTTerm>	iterateTerms()	Returns an iterator over all terms present in this formula.
Iterator<com.logic.exps.asts.others.ASTVariable>	iterateUnboundedVariables()	Returns an iterator over all unbounded (free) variables in this formula.
Iterator<com.logic.exps.asts.others.ASTVariable>	iterateVariables()	Returns an iterator over all variables in this formula, including both bounded and unbounded variables.

Methods inherited from interface com.logic.api.IFormula

getAST, hasGenerics, iterateGenerics

Method Details

iterateFunctions

Iterator<com.logic.exps.asts.others.ASTFun> iterateFunctions()

Returns an iterator over all function symbols used in this first-order logic formula. Functions represent mappings from terms to other terms (e.g., f(x), g(a, b)).

Returns:

An iterator over function symbols in the formula.

iteratePredicates

Iterator<com.logic.exps.asts.others.ASTPred> iteratePredicates()

Returns an iterator over all predicate symbols used in this first-order logic formula. Predicates define relations between terms (e.g., P(x), Father(x, y)).

Returns:

An iterator over predicate symbols in the formula.

iterateBoundedVariables

Iterator<com.logic.exps.asts.others.ASTVariable> iterateBoundedVariables()

Returns an iterator over all bounded variables in this formula. A bounded variable is one that is bound by a quantifier (e.g., ∀x, ∃y).

Returns:

An iterator over bounded variables in the formula.

iterateTerms

Iterator<com.logic.exps.asts.others.AASTTerm> iterateTerms()

Returns an iterator over all terms present in this formula. Terms include variables, functions, and constants that make up the logical expression.

Returns:

An iterator over terms in the formula.

iterateVariables

Iterator<com.logic.exps.asts.others.ASTVariable> iterateVariables()

Returns an iterator over all variables in this formula, including both bounded and unbounded variables.

Returns:

An iterator over all variables in the formula.

isABoundedVariable

boolean isABoundedVariable(com.logic.exps.asts.others.ASTVariable variable)

Determines whether the specified variable is a bounded variable in this formula.

Parameters:

variable - The variable to check.

Returns:

true if the variable is bounded, false otherwise.

isAnUnboundedVariable

boolean isAnUnboundedVariable(com.logic.exps.asts.others.ASTVariable variable)

Determines whether the specified variable is an unbounded variable in this formula.

Parameters:

variable - The variable to check.

Returns:

true if the variable is unbounded, false otherwise.

isAVariable

boolean isAVariable(com.logic.exps.asts.others.ASTVariable variable)

Determines whether the specified variable exists in this formula (either bounded or unbounded).

Parameters:

variable - The variable to check.

Returns:

true if the variable is present in the formula, false otherwise.

appearsFreeVariable

boolean appearsFreeVariable(com.logic.exps.asts.others.ASTVariable variable)

Determines whether the specified variable is a free variable in this formula. A free variable is an unbounded variable that is not within a quantifier's scope and occurs in the formula.

Parameters:

variable - The variable to check.

Returns:

true if the variable is free, false otherwise.

isFreeVariable

boolean isFreeVariable(com.logic.exps.asts.others.ASTVariable variable)

Checks whether a variable is free (not bounded) in the formula.

Parameters:

variable - The variable to check.

Returns:

true if the variable is free, false otherwise.

iterateUnboundedVariables

Iterator<com.logic.exps.asts.others.ASTVariable> iterateUnboundedVariables()

Returns an iterator over all unbounded (free) variables in this formula. Unbounded variables are not restricted by any quantifier.

Returns:

An iterator over unbounded variables in the formula.

isASentence

boolean isASentence()

Checks whether this first-order logic formula is a sentence. A sentence is a formula that contains no unbounded variables.

Returns:

true if the formula is a sentence, false otherwise.