The module provides the tools for applying Herbrand works over First Order Logic
It calculates the signature of an opened formula
It calculates the signature of a set of opened formulas
It generates the Herbrand Universe of n-order according to a Signature
It generates the Herbrand Universe of an opened formula
It generates the Herbrand Universe of a set of opened formulas
It generates a the Herbrand Base of n-order from a signature. That is, the set of all possible atoms for a signature wich corresponds to the applicatiion of each symbol of predicate (of arity k) over each k-tuple of elements of n-order universe Herbrand
It generates a the Herbrand Base of n-order from an opened formula. That is, a set of all posible atoms formed with the predicate symbosl of a formula, cosidering all the posible substitutions with the n-order Herbrand Unviverse elements.
It generates a the Herbrand Base of n-order from a set of opened formulas. That is, a set of opened and closed formulas where all posible substitutions with the n-order Herbrand Unviverse elements.
It generates all the possible Herbrand Interpretations of n-order from a signature. That is, all the possible subsets of the n-order Herbrand Basis associated to the signature.
It generates all the possible Herbrand Interpretations of n-order from a opened formula. That is, all the possible subsets of the n-order Herbrand Basis associated to the formula
It generates all the possible Herbrand Interpretations of n-order from a set of opened formulas. That is, all the possible subsets of the n-order Herbrand Basis associated to the formula
It valuates a Formula regarding to a Herbrand Interpretation and Herbrand Universe
It valuates a set of opened formulas regarding to a Herbrand Interpretation and Herbrand Universe
It searches Herbrand Models of n-order from a opened formula.
It searches Herbrand Models of n-order from a set of opened formulas.
It calculates the n-order Herbrand Extension vinculated to an opened formula. That is it gives a set of propositional formulas partially equiconsistent with the FOL formula
It calculates the n-order Herbrand Extension vinculated to a set of opened formulas. That is it gives a set of propositional formulas partially equiconsistent with the FOL formula
A signature is a 3-tuple with the constants, the functions symbols with its arity and the predicate symbols with its arity that apears in one (or a set of) opened formula(s).