Unavailable. Nobody can download this version any more, with elm or with the Lamdera compiler: github.com/vicramgon/logicus is gone (deleted or private); Software Heritage not asked yet (this run's --swh-calls were used up); no fork with tag 10.0.0 found (12 same-name repos checked); no cached copy. Use another version.
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).