AUTOMATIC REASONING

"Causality does not operate backwards" (Gregory Bateson).

"Logic was born as an attempt to mechanize the intellective processes of reasoning" (D. Hofstadter).

"Mathematics will soon be done only by computers" (Boris Shaliach).

"Logic is combining the known to reach the unknown" (George Edward Moore).

---

Types of Reasoning
Reasoning as a mode of analytical consciousness

As we know, there are two modes of consciousness:

• Descending (top-down), deductive, analytical or syntactic. It goes from the general to the particular, from the deep to the superficial. It corresponds to the mode of the left hemisphere (HI) of the brain.
  
  
• Ascending (bottom-up), inductive, synthetic or semantic. It goes from particular to general facts (or from general to more general or universal), from the superficial to the deep. The human mind, in its synthetic aspect, conceptualizes, always looking for the most general categories to the particular facts in order to make reality intelligible. If it does not find them, it looks for a secondary pattern that relates the categories. Induction can be complete (when all cases are examined) or incomplete (when not all cases are examined). It corresponds to the right hemisphere (HD) mode of the brain.

Reasoning is using the HI mode, going from the general to the particular, the ability to make inferences or deductions. To do this, everything must be expressed in formal language. Reasoning makes explicit knowledge that is already implicit in the premises or knowledge base.


The automaticity of reasoning

The incomplete inductive consciousness in principle cannot be automated because the intuitive cannot be formalized; only its manifestations can be formalized. Synthetic consciousness is the object of study of cognitive psychology, being today one of the main challenges of artificial intelligence.

Analytic consciousness, on the other hand, can be automated, since it is purely formal. Automatic reasoning is a branch of computer science that studies the reasoning capabilities of computational systems.


The concept of inference

Inference is the process of deriving conclusions from a set of premises (or deriving theorems from axioms). The premises, the conclusions, and the process of inference itself must be expressed in a formal language, which may be natural or artificial. The premises or axioms can be of general or specific type, as well as the conclusions.

Assuming that the process of inference is correct, the inferences may be valid, even if the premises are false. But true inferences always follow from the truth of the premises.

An inference is monotonic if it does not vary by adding new premises. Otherwise, it is non-monotonic.


Types of reasoning with rules

A knowledge base consists of:

1. A set of premises or axioms of a theory, expressed in a formal language. If these premises are expressed by rules of the type "condition → action" or "antecedent → consequent", we have a rule base, representing generic knowledge.
   
   
2. A set of facts, which form a fact base. They represent specific knowledge.

In this knowledge base there are two types of reasoning:

1. Direct (or forward).
   The antecedents of the rules are examined, and when they are satisfied, inferences are drawn, which are the consequents. The rules are reapplied to the inferences obtained to obtain new inferences. And so on until the rules produce no new inferences.
   
   
2. Inverse (or backward).
   We start from the target (a sentence or expression) and examine the rules containing that target in the consequents of the rules. If no rules are found, it is impossible to reach the target. If they are found, one of them is chosen and the antecedent of that rule becomes the new objective. And so on in a recursive process. When a rule does not lead to the goal, another alternative rule is chosen (if it exists). This type of reasoning is the one used in logic programming.

These two types of reasoning are analogous to those used in arithmetic calculus. For example: 1) Direct: 3² = 9 (the operation of raising 3 to the square is performed); 2) Inverse: √9 = 3 (a number such that its square is 9 is sought),

Direct reasoning is easier to automate than inverse reasoning, just as it is easier to perform direct operations than inverse ones.

The advantage of direct reasoning is that all the expressions being inferred are incorporated into the knowledge base. The disadvantage is that the inferred expressions are the basis for further inferences, a process that tends to grow exponentially.

The advantage of inverse reasoning is that we know the objective, the expression to prove, and we avoid exploring unnecessary rules. The disadvantage is that the steps we are taking are not guaranteed, having to backtrack often to find the correct path that will lead us to the goal. When applicable, inverse reasoning is more efficient than direct reasoning because you don't have to make multiple passes through the set of rules.

Ideally, both methods should be used in a controlled manner, depending on the issue or problem at hand.


The management of automatic reasoning

The management of reasoning, both direct and inverse, is performed with a reasoning program or "engine". This engine can be specific to each particular system or it can be generic (or universal), valid for any system. Ideally, a universal engine can be developed, i.e., regardless of the content of the rules.

Automatic reasoning is independent of the mechanical device with which it is implemented. Computing is an activity that can be human or mechanical, but conceptually it is the same thing. Informatics or computer science is not reducible to computer technology any more than astronomy is reducible to telescope technology. Computers and telescopes are just instruments of their respective sciences.

The reasoning engine performs two functions:

1. The examination of each rule to see if it is applicable. If the engine is direct reasoning, it examines the antecedent. If the engine is inverse reasoning, it examines the consequent. The inference engine for forward reasoning explores the rules in breadth, i.e., all rules, independent of each other, are considered. For backward reasoning, the rules are examined in depth, i.e., one starts from a rule and looks for a rule dependent on it.
   
   
2. Control, which manages the order in which rules are examined.

Automatic proof of theorems

Automatic theorem proving (DAT) −in English, Automated Theorem Proving, ATP− is a type of inverse reasoning. It is based on formal logic. It is currently the most developed field of automated reasoning.

The procedure consists of 3 steps: 1) the user expresses a conjecture using a formal language expression; 2) this expression is passed to the computational system as input; 3) the system attempts to solve it; 4) if it is solved, the answer can be positive or negative (the conjecture is or is not a theorem).

A theorem provers starts from the theorem to be proved and the demonstrator discovers (or infers) the steps to be performed to get from the axioms to the theorem.

A demonstration can serve to prove that something is true or to prove that something is false. To refute is to prove a negation.

By automating the proof of theorems, new theorems not previously known have been found. Some shorter and more elegant demonstrations than human ones have also been discovered.


Fields of application

The fields of application of automatic reasoning are numerous, the most important being:

• Mathematics. Demonstration of mathematical theorems in Boolean algebra, group theory, lattice theory, algebraic geometry, combinatorial logic, etc.
  
  
• Computer science. Database design and management, program generation and verification, logic programming.
  
  
• Artificial intelligence. Expert systems, knowledge engineering, robotics, intelligent agents.
  
  
• Internet. Semantic Web.
  
  
• Electrical circuits. Design and verification of integrated circuits (e.g., to verify that mathematical operations have been designed correctly, especially more complex operations such as floating point operations.
  
  
• Linguistics. Natural language processing.

A brief history of automatic reasoning

• The theory of formal deduction was born with Aristotelian syllogistic logic, realized in natural language.
  
  
• Towards the end of the 17th century, Leibniz postulated the need for a universal formal language (Lingua Characteristica Universalis) to be able to express any idea. This language should also serve to mechanize any kind of reasoning (Calculus Ratiocinator). Leibniz claimed that reasoning is like calculus, and that instead of long discussions, it would be better to sit down and calculate to determine who was right in each case.
  
  Leibniz believed that a coherent system of logic and mathematics could be formalized by means of a language consisting of an alphabet of symbols manipulated by mechanical rules. Anticipating what we now call "software", he claimed that logic and mathematics could be mechanized. With his Calculus Ratiocinator, Leibniz believed that all truths of reason could be discovered mechanically.
  
  According to Leibniz, our universe would have been created by a minimum number of laws leading to a maximum diversity. That binary arithmetic embodied that principle: only two signs suffice to write all numbers; the finite begets by combinatorics the infinite. That binary coding was the key to universal language, since it not only made it possible to represent numbers but also the logic of dichotomies. That through digital computation mankind would have a powerful instrument to increase the power of the mind.
  
  
• In 1847, George Boole invented the algebra of logic (reducing logic to algebra), a first step towards the mechanization of logical thought processes.
  
  
• In 1879, Frege published his Begriffsschrift (Conceptography), giving birth to formal logic, modern mathematical logic with the predicate calculus. His work "Fundamentals of Arithmetic" (published in 1884) expressed it through formal logic, inaugurating the logicist current of mathematics (logic as the foundation of mathematics).
  
  
• In 1889, Peano published Arithmetices Principia, in which he used a symbolic notation to formalize arithmetic, a first-order theory of the properties of the natural numbers.
  
  
• At the beginning of the 20th century, Cantor invented set theory. Mathematical language is reduced and grounded in predicate logic and set theory.
  
  
• Also at the beginning of the 20th century, Hilbert proposed to found mathematics by means of a metamathematical system, a universal axiomatic system, from which all mathematics would be derived. According to Hilbert, all mathematics can be deduced from a universal axiomatic system consisting of a few axioms and a few rules of inference. Hilbert had invented a formal axiomatic system for propositional logic based on 3 axioms and a rule of inference (see Addendum).
  
  
• In the years 1910-1913, Russell and Whitehead, following the logicist line inaugurated by Frege, published Principia Mathematica, a work that was revised (in a second edition) in 1927. These authors believed that they could derive all mathematics from only 4 logical axioms, 3 axioms of set theory and 2 transformation rules.
  
  
• In 1929, Gödel proves that first-order predicate logic is complete, i.e., that every valid formula is provable. Valid formulas are recursively numerable.
  
  
• In 1929, Mojzesz Presburger proves that the theory of natural numbers with addition and equality is decidable, and gave an algorithm for determining whether a given sentence of the language was true or false.
  
  
• In 1930, Jacques Herbrand published the paper "Investigation in proof theory" [Herbrand, 1930]. In it he proposes an automatic method for proving theorems of first-order predicate logic. This method produced an exponential growth of inferences (the so-called "Herbrand universes").
  
  
• In 1931, Gödel published his incompleteness theorem, in which he proved that a formal axiomatic system including the natural numbers is incomplete: there are undecidable sentences (it is not possible to prove their truth or falsity). Gödel used to prove this a self-referential expression, an expression impossible to reach through the axioms, however numerous they may be. Gödel's theorem invalidates logicism in general and the projects of Hilbert and of Principia Mathematica in particular.
  
  
• In 1934, Gerhard Gentzen invented Natural Deduction and the Calculus of Sequents, a theory and practice aimed at emulating human reasoning in mathematical proofs. The semantic level is higher than Boolean algebra, but the proofs are more complex. Gentzen broke the traditional axiomatic formalization of Frege, Hilbert and Russell.
  
  
• After World War II, electronic computers appeared, and with the advances in mathematical logic, the subject of automatic reasoning was taken up again with force, becoming one of the main topics of artificial intelligence.
  
  
• In 1957, Allen Newell, Herbert Simon and Clifford Shaw presented their Logic Theorist Machine, a computer program that was able to prove 38 of the 52 theorems of propositional logic of Russell and Whitehead's Principia Mathematica. This program was the first artificial intelligence program and used a small number of axioms and heuristic inference rules.
  
  
• In 1959, P.C. Gilmore, using disjunctive normal forms (disjunction of conjunctions), achieved many automatic proofs of formulas of first-order logic (without equality) by the method of reducing a first-order formula to another propositional formula associated with it [Gilmore, 1959].
  
  
• In 1960, Martin Davis and Hillary Putnam published "A computing procedure for quantification theory", in which they proposed a complete inference algorithm or procedure for formulas expressed in conjunctive normal form (conjunction of disjunctions) [Davis & Putnam, 1960]. They introduced the concept of "clause" (a disjunction of formulas with predicates, affirmative or negative, universally quantified) and reduced first-order demonstrations to the study of the consistency of finite sets of propositional clauses, by means of simplifying rules. However, the algorithm generated too large a search space.
  
  
• In 1960, Hao Wang developed a computer program with which he succeeded in proving 220 theorems of Principia Mathematica, including theorems of first-order predicate logic, using Gerhard Gentzen's system of natural deduction (calculus of sequents without cutting rules). His method was more refined than that of Davis and Putnam, and his program was more efficient than that of the theoretical logic machine because it used heuristics [Wang, 1960, 1970].
  
  
• In 1965, John Alan Robinson published "A machine-oriented logic based on the Resolution Principle" [Robinson, 1965], where he introduced the Resolution Principle, a method that significantly reduces the reasoning process efficiently. The axioms are expressed in disjunctive form. He uses the refutational method (reductio ad absurdum): one starts from the negation of what one wants to prove, and if a contradiction is reached, the theorem is true.
  
  Robinson's method is consistent and complete. "Complete" means that if we have a set of statements and unsatisfiable (false), the resolution method derives the empty clause, indicating that a contradiction exists.
  
  The resolution principle is very simple, since it is based on a single rule, in which two parent clauses are replaced by a resolvent clause:
  
  
  Premises: A∨B and ¬A. Conclusion: B.
  
  This rule generalizes on the principle of binary resolution:
  
  
  Premises: A∨B and ¬A∨C. Conclusión: B∨C.
  
  And its more general form is:
  
  
  Premises: A∨B₁∨… ∨B_n y ¬A∨C₁∨…∨C_m. Conclusión: B₁∨…∨B_n∨C₁∨…∨C_m.
  
  Along with the resolution method, Robinson presented a unification algorithm, which maximized the generality of the inferences. The unification algorithm identifies pairs of complementary terms (a constant and a variable) and performs a substitution (of the variable for the constant) to eliminate the differences. It is a recursive algorithm: it generates resolvents, resolvents of resolvents, etc., until the empty clause is reached.
  
  Robinson's method was a milestone and gave a great impetus to the subject of automatic theorem proving. However, Robinson's method has several limitations:
  
  
  1. It can work in first-order predicate logic, but provided that free variables (those that can have any value), which are implicitly universally quantified, are used.
     
     
  2. It does not work with higher-order logic.
     
     
  3. In practice, there is a "population explosion" of clauses,including irrelevant or redundant clauses, so the search space to find a solution is very large (even for proving simple theorems), so that sometimes a solution is not reached in reasonable time.
  
  Robinson's method of solving has been improved (refined) over the years and has led to a variety of heuristics (also called "strategies") for reducing the search space. One way to reduce the search space is to restrict the inference rule so that fewer inferences are generated, but maintaining the completeness of the procedure.
  
  
• In 1970 the 4-color theorem (4 colors are enough to color a map) was proved by a computer program that exhaustively examined all possible types of combinations. It was a matter of great controversy, since it was the first automatic proof that was impossible to verify at the human level due to the enormous size of the calculations performed by the program.
  
  
• In the early 1970s, inspired by Robinson's method of solving, Robert Kowalski introduced logic programming, paving the way for the Prolog language [Kowalski, 1979].

A European research initiative in the field of efficient and accurate theorem proving is underway. The project is called TPTP (Thousands of Problems for Problem Solvers, http://www.tptp.org). A new language also called TPTP has been created in which to express problems and solutions using higher-order logic. And also a format called THF (Typed Higher-order Form).

Today, Leibniz's ideal can be considered to have been largely achieved. However, there is still much to be done: researching new heuristics, new more efficient algorithms, new rules (or meta-rules), etc.

Today there is no discussion of arithmetic when using a calculator. But the calculator, even if it gives the correct answer, does not prove it, i.e., it does not show all the steps it takes to arrive at a result. Ideally, reasoning should achieve the same result.


MENTAL and Automatic Reasoning
Traditional automatic reasoning systems are based:

• On propositional logic or first-order predicate logic.
  
  
• The generic knowledge base is limited to rules.
  
  
• An inference engine is needed to manage the generic knowledge base from the specific knowledge base and produce the inferences.

In contrast, in MENTAL:

• Expressions can be of any type, not only logical. Moreover, logical expressions can have predicates of any order.
  
  
• The generic knowledge base is based on generic expressions.
  
  
• No inference engine is needed because the inferences are automatic by the semantics of the generic expressions themselves.

Actually, the problem of inferences can be stated in a general way. An inference process is a normal evaluation process of an expression that produces a modification of the abstract space. If the original expression does not change, all new expressions generated are the inferences produced.


Universal language

The problem with automatic reasoning is that it is not possible to address it in a coherent way without a standard, universal formal language, where the mathematical-logical language is equal to that of computers. With MENTAL as a universal language, this problem disappears and we are in ideal conditions to address the issue of automatic reasoning.

Traditionally, in automatic reasoning, a formal language based on first-order predicate logic with equality has been considered, a language with which many areas of mathematics could be formalized. But this language is far from universal and is not the language of computers.

Characteristics of MENTAL as a universal language for automatic reasoning are:

• It uses generic expressions, which have an enormous integrating and unifying power. Generic expressions (parameterized or not) allow to perform automatic reasoning (direct and inverse) because they perform the examination and control of the rules from a higher level. No forward or backward "reasoning engine" is needed because the engine is implicit in the language. It also allows heuristics to be expressed.
  
  
• Logic is based on the "Condition" primitive. Negation, conjunction and disjunction are derived operations. Higher order logic can also be used.
  
  
• Predicates are external attributes or qualifiers that can be applied to any expression. For example, "Socrates/mortal." Properties are internal qualities (e.g., the property of a noun beginning with "A", the property of a noun having length 4, or the property of a number being greater than 3), etc.
  
  
• There are no logical quantifiers. The role of the universal quantifier is played by a parameter of a generic expression. The existential quantifier is a property (the cardinality) of a set or sequence.
  
  
• There are no specific conditional expressions. Antecedent and consequent of a condition can be any expressions.
  
  
• It does not consider traditional logical values (true and false). Instead it contemplates existential values (existence and non-existence). It does not consider the issue of truth but only the issue of the existence or non-existence of an expression.
  
  
• A clear distinction is made between particular and general expressions.
  
  
• Equivalence and substitution are used along with the rest of the semantic primitives.
  
  
• Inference can be dynamic, in the sense that inferences vary when expressions change.

The formalization of a demonstration

Traditionally, the premises and conclusion are represented vertically:

A₁
,,,
A_n
---------
C

For example, Robinson's binary resolution rule is expressed as follows:

A∨B
¬A∨C
---------
B∨C

The problem with this representation is that no formal language relating premises and conclusion is used.

In MENTAL, this problem is easily solved by the semantics of the "Condition" operation. For example, Robinson's rule above can be expressed as a generic expression:

⟨( A∨B → ¬A∨C → B∨C)⟩

This expression is equivalent to
⟨( (A∨B ∧ ¬A∨C) → B∨C)⟩
Where ⟨( ¬A = (A?)' )⟩


The coding of the rules

In order to make the process as efficient as possible and to correspond to the type of reasoning to be performed, the rules are specified by means of generic expressions as follows:

• Forward reasoning:
  ⟨( A1 → ... → An → C )⟩
  
  
• Backward reasoning:
  ⟨( C ← A1 ← ... ← An )⟩

with Ai being the antecedents and C being the consequent. These expressions have the advantage that when an antecedent is not satisfied, the analysis process of that rule is terminated. This is called "cutting".

In forward reasoning it goes from antecedents to consequents. Backward reasoning goes from the consequent to the antecedents.

Since evaluation is from left to right, in backward reasoning you put what you want to prove first.

There can be several expressions with the same C, that is to say, that there are alternatives: the conclusion can be reached by several possible ways. And the same thing happens with antecedents.

This rule structure is equivalent to Horn's clauses, the one used in logic programming, which have the form.

c ← a₁, a₂, ... , a_n or, a₁, a₂, ... , a_n → c

where commas assume logical "and" connections (and).

Rules can interact with each other such as being activated or deactivated, constrained with additional conditions, and so on.


Types of inferences

Inferences are made using the condition operators (→, ← and ↔), the substitution operators (=, =: and :=) and the equivalence operator (≡).

Inferences go from the general to the particular and can be of two types:

1. Horizontal. They are made through the symmetric operators (↔ and ≡).
   
   
2. Vertical descending. They are realized through condition and substitution operations.

Types of expressions

In MENTAL we can classify expressions into 3 types:

1. Expressions type A. These are the generic expressions (parameterized or not), which are the engines of the inferences.
   
   
2. Expressions type B. These are generic (parameterized or not) or non-generic expressions that are the initial expressions from which inferences are made.
   
   
3. Expressions type C. These are the inferences made by means of the expressions of the two previous types.

Expressions of type B are specified after those of type A so that they are evaluated immediately and produce expressions of type C.


Characteristics of inferences

• There may be no expressions of type B, i.e., expressions of type A are sufficient for making inferences.
  
  
• Every MENTAL expression is evaluated and may or may not generate inferences. Inferences (C) may be general or particular expressions, depending on the generic expressions A and B. One expression can give rise to several inferred expressions.
  
  
• There may be no expressions of type C (null inferences), that is, there are no new expressions.
  
  
• In MENTAL not only logic is used, but any generic expression involving the above operators. Inference is implicit in the semantics of generic expressions.
  
  
• In MENTAL, inferences can be monotonic or non-monotonic, depending on the expressions used. Non-monotonic means that inferences may vary as A expressions or B expressions are modified.
  
  In general, inferences are dynamic, in the sense that an expression X can infer another expression Y, and subsequently the same expression X infer another different expression Z or infer nothing.
  
  
• In inference, exponential growth of expressions in abstract space can occur, but today this problem is not too important because of the cheapening of memory and the growth of computer processing power. In addition, constraints can be imposed to limit automatic inferences, including heuristics or additional conditions to generic expressions.
  
  
• There is no search process. It is just a matter of knowing whether or not an expression exists in the abstract space. Search is an implementational issue. At the conceptual level, generic expressions are sufficient.

Examples

1. Expressions type A.
   ⟨( x/man → x/mortal )⟩ // modus ponens
   
   Expressions type B.
   Socrates/man
   
   C type expressions (inferences).
   Socrates/mortal
   
   
2. Expressions type A.
   ⟨( a = b )⟩ // substitution
⟨( b = c )⟩ // substitution
   
   Expressions type B.
   None.
   
   Expressions type C (inferences).
   ⟨( a = c )⟩ // transitive law of substitution
   
   
3. Expressions type A.
   ⟨( x+y ≡ y+x )⟩ // commutative law of addition
   
   Expressions type B.
   a+b
⟨a+x⟩
   
   Expressions type C (inferences).
   (a+b ≡ b+a)
(⟨a+x⟩ ≡ ⟨x+a⟩)
   
   
4. Expressions type A.
   ⟨( x → x∨y )⟩ // law of logic
   
   Expressions type B.
   a
   
   Expressions type C (inferences).
   ⟨( a → a∨y )⟩
   
   
5. Expressions type A.
   ⟨( x*y ≡ y*x )⟩ // commutative law of the product

⟨( (x+y)*z ≡ (x*z + y*z) )⟩ // distributive law
   
   Expressions type B.
   None.
   
   Expressions type C (inferences).
   ⟨( (x+y)*z ≡ (z*x + z*y) )⟩
⟨( (x+y)*z ≡ (x*z + z*y) )⟩
⟨( (x+y)*z ≡ (z*x + y*z) )⟩
⟨( (x+y)*z ≡ (x*z + y*z) )⟩

⟨( z*(x+y) ≡ (x*z + y*z) )⟩
⟨( z*(x+y) ≡ (z*x + z*y) )⟩
⟨( z*(x+y) ≡ (x*z + z*y) )⟩
⟨( z*(x+y) ≡ (z*x + y*z) )⟩
   
   This is an example of inferences that produce generic expressions.
   
   
6. Expressions type A.
   ⟨( (x+y)*z ≡ (x*z + y*z) )⟩ // distributive law

⟨( x^2 =: x*x )⟩
   
   Expressions type B.
   (a+b)^2
   
   Expressions type C (inferences).
   ( (a+b)^2 =: (a^2 + 2*a*b + b^2) )
   
   
7. Expressions type A.
   ⟨( x∧y → x )⟩ // law of logic

⟨( x∧y ↔ y∧x )⟩ // commutative law of the logical conjunction
   
   Expressions of type B.
   a∧b
   
   Expressions type C (inferences).
   b∧a
a
b
   
   
8. Expressions type A.
   ⟨( x∈(C∩D) ↔ (x∈C ∧ x∈D) )⟩
   
   Expressions type B.
   a∈(A∩B)
   
   Expressions type C (inferences).
   a∈A
a∈B
   
   
9. Expressions type A.
   ⟨( (x ∨ y) ≡ (x' ∧ y')' )⟩ // De Morgan's first law

⟨( (x ≡ y') ↔ (x' ≡ y) )⟩
   
   Expressions type C (inferences).
   ⟨( (x ∨ y)' ≡ (x' ∧ y') )⟩

⟨( (x' ∨ y')' ≡ (x ∧ y) )⟩ // second Morgan's law

Management of generic expressions

• Activation/deactivation of a generic expression.
  You can control the inferences of generic expressions by using a variable indicating the activation or not of such generic expressions. For example:
  
  ⟨( k=1 → ⟨( f(x) = (2^x + 1) )⟩ )⟩
  k=1 // activate generic expression ⟨( f(x) = (2^x + 1) )⟩ )⟩

f(3) // ev. 7

k=0 // disable generic expression

f(3) // evaluate itself
  
  
• Substitution of a generic expression G1 by another G2:
  
  
  ( p = G1 )
⟨p⟩
( p = G2⟩ )
  
  
• Removal of a generic expression G.
  
  
  ( p = G )
⟨p⟩
( p = θ⟩ )

Example of direct and inverse reasoning

We start from a (well-formed) expression G, generic (parameterized or not) or specific, of which we want to know if it is valid or not.

The process is automatic, since generic expressions are evaluated at all times. Therefore, if G appears as a consequent in some axiom, it will automatically evaluate itself if the associated condition is satisfied. If that condition in turn depends on another condition, the same process applies, and so on. Conditions that are not satisfied will be evaluated as (the null expression). Example:

We define (P(x) = y) as "the parent of x is y".

We define (H(x) = y) as "the child of x is y".

We define (A(x) = y) as "the grandfather of x is y".

Knowledge base for direct reasoning:

Facts:
(P(a) = b) (P(b) = c)

Rules:
⟨( (P(x) = y) ↔ (H(y) = x) )⟩
⟨( (P(x) = y) → (P(y) = z) → (A(x) = z))⟩

Knowledge base query:

(A(a) = c)? // ev. α
(A(a) = b)? // ev. θ

Knowledge base for inverse reasoning:

(P(a) = b) (P(b) = c)
⟨( (A(x) = y) ← {⟨( z ← (P(x) = z) → (P(z) = y) )⟩}# > 0) )⟩

Knowledge base query:

(A(a) = c)? // ev. α
(A(a) = b)? // ev. θ

Conclusions

Leibniz's idea of creating a universal language can be said to have been fulfilled with MENTAL, being founded on a minimal number of concepts that produce potentially infinite expressions. But it is not founded on the binary calculus, but on dual primary archetypes. Duality is universal. Binary numbers are only the simplest manifestation of that duality.

And Leibniz's idea of that universal language being able to perform computations has also been realized with MENTAL. Those computations are specified by generic expressions, which are self-sufficient as engines for automatic reasoning.

---

Addenda
Hilbert's deductive system

Hilbert's deductive system for propositional logic has the following characteristics:

• It consists of only 3 axioms (tautologies) in which only the logical connectives "¬" and "→" are considered:
  
  
  1. p→(q→p)
  2. (p→(q→r))→((p→q)→(p→r)) (distribución)
  3. (¬p→¬q)→((¬p→q)→p)
  
  
• It has only one rule of inference: the Modus Ponens: p, p→q ⇒ q.
  
  
• A formal deduction is a finite sequence of formulas of propositional logic where each formula is an instance of an axiom or the application of the rule of inference to two previous formulas.

For example, we want to prove: p→p:

1. Instantiation of axiom 1 with p=p and q=(p→p): p→((p→p)→p)
   
   
2. Instantiation of axiom 2 with p=p, q=(p→p) and r=p: p→((p→p)→p))→
   ((p→(p→p))→(p→p))
   
   
3. Applying the Modus Ponens between 1 and 2: (p→(p→p))→(p→p)
   
   
4. Instantiated axiom 1 with p=p and q=p: p→(p→p)
   
   
5. Applying the Modus Ponens between 3 and 4: (p→p)

Bibliography

• Bibel, W. Automated Theorem Proving. Vieweg Verlag, 1987.
  
  
• Bledsoe, W.W. Non-resolution theorem proving. Artificial Intelligence 9(1), 1977.
  
  
• Boyer, R.S.; Moore, J.S. A Computational Logic Handbook. Academic Press, 1988.
  
  
• Buss, Samuel R. An introduction to proof theory. En Buss, Samuel R. (ed.), Handbook of proof theory, pp. 1-78, Elsevier 1998.
  
  
• Chang, C.L., Lee, R.C.-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1997.
  
  
• Cuena Bartolomé, José. Lógica Informática. Alianza Editorial, 1985.
  
  
• Gardner, Martin. Máquinas y diagramas lógicos. Alianza Editorial, 1985.
  
  
• Gilmore, P.C. A procedure for the production from axioms, of proofs for theories derivable within the first order predicate calculus. Proc. IFIP Congr. 1959, pp. 265-273, 1959.
  
  
• Hogger, C.J. Introduction to Logic Programming. Academic Press, 1984.
  
  
• Kowalski, Robert. Logic for Problem Solving. Elsevier, 1979.
  
  
• Kowalski, Robert. Lógica, Programación e Inteligencia Artificial. Diaz de Santos, 1986.
  
  
• Kowalski, Robert. The case for using equality axioms in automatic demostration. Lecture Notes in Maths, 125: 112-127, 1970.
  
  
• Lassez, Jean Louis; Plotkin, Gordon (eds.). Computational Logic. Essays in Honor of Alan Robinson. The MIT Press, 1991.
  
  
• Loveland, D.W. Automated Theorem Proving. A Logical Basis. North Holland, 1978.
  
  
• Nilsson, N.J. Problem Solving Methods in Artificial Intelligence. McGraw Hill, 1971.
  
  
• Portoraro, Frederic, Automated Reasoning. En Edward N. Zalta, Stanford Encyclopedia of Philosophy.
  
  
• Robinson, John Alan. A machine-oriented logic based on the resolution principle. J. ACM 12 (1): 23-41, 1965.
  
  
• Robinson, John Alan. Automated Deduction with Hyperresolution. International Journal of Com. Mach, 1: 227-234, 1965.
  
  
• Robinson, John Alan; Voronkov, Andrei (eds.). Handbook of Automated Reasoning. The MIT Press, 2001.
  
  
• Robinson, John Alan. Computational Logic: The Unification Computation. Internet, 1971.
  
  
• Slagle, J.R. Automatic Theorem Proving with Renamable and Semantic Resolution. JACM 14: 687-697, 1967.
  
  
• Tarski, Alfred. Introduction to Logic and the Methodology of Deductive Sciences. Dover, 1995.
  
  
• Veroff, Robert (ed.). Automated Reasoning and Its Applications. Essays in Honor of Larry Wos. The MIT Press, 1997.
  
  
• Wang, Hao. Proving Theorems by Pattern Recognition I. Communications of the ACM, 3: 220-234, 1960. Disponible online.
  
  
• Wos, Larry. Automated Reasoning: Introduction and Applications. McGraw-Hill, 1992.
  
  
• Wos, Larry. J.A. Robinson, a review of Automatic Theorem-Proving. Journal of Symbolic Logic 39 (1): 190, 1974.
  
  
• Wang, Hao. Logic, Computers, and Sets. Chelsea Pub. Co., 1970.