TERMIUM Plus^®

Fiche 1,  Justifications,  Anglais

Record number: 1, Textual support number: 1 CONT

[Researchers] introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations guided by reinforcement learning from previous proof attempts.  2, fiche 1, Anglais, - theorem%2Dproving%20algorithm

Fiche 1,  Justifications,  Français

Fiche 1,  Justifications,  Espagnol

Fiche 2,  Justifications,  Anglais

Record number: 2, Textual support number: 1 DEF

A normal form for predicate calculus formulae borrowed from mathematical logic, and much used in automatic theorem proving.  2, fiche 2, Anglais, - clausal%20form

Record number: 2, Textual support number: 1 CONT

The logic used to represent knowledge in logic programming is clausal form which is a subset of first-order predicate logic.  3, fiche 2, Anglais, - clausal%20form

Fiche 2,  Justifications,  Français

Record number: 2, Textual support number: 1 CONT

On peut représenter une formule en forme normale conjonctive par un ensemble de clauses, on parle alors de forme clausale.  2, fiche 2, Français, - forme%20clausale

Fiche 2,  Justifications,  Espagnol

Fiche 3,  Justifications,  Anglais

Record number: 3, Textual support number: 1 OBS

See also the record "theorem proving".  2, fiche 3, Anglais, - proving%20procedure

Fiche 3,  Justifications,  Français

Record number: 3, Textual support number: 1 OBS

Voir aussi la fiche "démonstration de théorèmes.  2, fiche 3, Français, - proc%C3%A9dure%20de%20d%C3%A9monstration

Fiche 3,  Justifications,  Espagnol

Fiche 4,  Justifications,  Anglais

Record number: 4, Textual support number: 1 DEF

A proposition proved, or sometimes assumed, to be true and used in proving a theorem.  2, fiche 4, Anglais, - lemma

Fiche 4,  Justifications,  Français

Record number: 4, Textual support number: 1 DEF

Énoncé de mathématique préliminaire nécessaire à la démonstration d'un théorème.  2, fiche 4, Français, - lemme

Record number: 4, Textual support number: 1 PHR

Lemme de comparaison, de poursuite, de Siegel, de théorème Kam.  2, fiche 4, Français, - lemme

Fiche 4,  Justifications,  Espagnol

Fiche 5,  Justifications,  Anglais

Record number: 5, Textual support number: 1 CONT

We begin the history of automated theorem proving by mentioning some programs that have proven theorems in areas other than the first-order predicate calculus. A 1956 program called the ’Logic Theorist’ or simply LT... proves theorems in propositional calculus(also called sentential calculus...).  2, fiche 5, Anglais, - logic%20theory%20machine

Fiche 5,  Justifications,  Français

Fiche 5,  Justifications,  Espagnol

Fiche 6,  Justifications,  Anglais

Record number: 6, Textual support number: 1 DEF

A resolution method that reaches conclusions using logic; it is normally done by theorem proving.  2, fiche 6, Anglais, - logical%20inference

Record number: 6, Textual support number: 1 CONT

Japanese planners want their machines to handle millions of logical inferences per second (LIPS) - one logical inference equalling one step in a syllogistic, or IF-THEN, sequence of reasoning.  3, fiche 6, Anglais, - logical%20inference

Record number: 6, Textual support number: 2 CONT

Each logical inference involves a set of premises, a reason, and a conclusion. ... The student is finished when there is a set of logical inferences connecting the given statements to the statements to be proved.  4, fiche 6, Anglais, - logical%20inference

Fiche 6,  Justifications,  Français

Record number: 6, Textual support number: 1 CONT

Lorsqu'il fallut formaliser des règles effectivement utilisées par les médecins, il fut évident que leurs inférences étaient moins des inférences logiques, (SI E alors H), que des inférences plausibles.  2, fiche 6, Français, - inf%C3%A9rence%20logique

Fiche 6,  Justifications,  Espagnol

Fiche 7,  Justifications,  Anglais

Record number: 7, Textual support number: 1 DEF

A layered family of software tools designed to enable the efficient and flexible use and development of significant theorem proving systems.  1, fiche 7, Anglais, - logic%20machine%20architecture

Fiche 7,  Justifications,  Français

Fiche 7,  Justifications,  Espagnol

Fiche 8,  Justifications,  Anglais

Record number: 8, Textual support number: 1 OBS

Reduction mechanism for theorem proving.  1, fiche 8, Anglais, - reduction%20mechanism

Fiche 8,  Justifications,  Français

Fiche 8,  Justifications,  Espagnol

Fiche 9,  Justifications,  Anglais

Record number: 9, Textual support number: 1 DEF

A process or philosophy that aids in the solution of a wide range of problems.  1, fiche 9, Anglais, - general%20heuristic

Record number: 9, Textual support number: 1 CONT

The process of working backward in theorem proving is a general heuristic.  1, fiche 9, Anglais, - general%20heuristic

Fiche 9,  Justifications,  Français

Record number: 9, Textual support number: 1 OBS

voir heuristique et heuristique spéciale.  1, fiche 9, Français, - heuristique%20g%C3%A9n%C3%A9rale

Fiche 9,  Justifications,  Espagnol

Fiche 10,  Justifications,  Anglais

Record number: 10, Textual support number: 1 CONT

These procedures [natural procedures for theorem proving] are quite different from the logically and syntactically detailed inference mechanisms resorted to by typical computer-based theorem provers.  1, fiche 10, Anglais, - computer%2Dbased%20theorem%20prover

Fiche 10,  Justifications,  Français

Record number: 10, Textual support number: 1 OBS

Voir démontreur de théorèmes.  1, fiche 10, Français, - d%C3%A9monstrateur%20de%20th%C3%A9or%C3%A8mes%20par%20ordinateur

Fiche 10,  Justifications,  Espagnol

Fiche 11,  Justifications,  Anglais

Record number: 11, Textual support number: 1 DEF

It represents proofs in a way that maintains a distinction between goals and antecedents, and it uses inference rules that mimic the reasoning of human theorem proving.  2, fiche 11, Anglais, - natural%20deduction%20system

Fiche 11,  Justifications,  Français

Fiche 11,  Justifications,  Espagnol