The Tableaux is a logical calculus tool that is very useful to demonstrate a conclusion from a set of premises, find counterexamples or models of a set of logical formulas or demonstrate that a formula is a tautology, i.e., that is true in all possible cases. They can be used in artificial intelligence as the basis for implementing automated theorem proving.
The Tableaux is a logical calculation tool that allows checking the validity of a conclusion from a series of premises. In the previous article I explained briefly the fundamentals of predicate logic Tableaux. In this article I will extend the program to the first-order logic, which has much more expressive capacity than predicate logic, although this makes also automatic calculation more difficult.