Titlebook: Automated Deduction - CADE-15; 15th International C Claude Kirchner,Hélène Kirchner Conference proceedings 1998 Springer-Verlag Berlin Heid

Enlightening

书目名称Automated Deduction - CADE-15影响因子(影响力)




书目名称Automated Deduction - CADE-15影响因子(影响力)学科排名




书目名称Automated Deduction - CADE-15网络公开度




书目名称Automated Deduction - CADE-15网络公开度学科排名




书目名称Automated Deduction - CADE-15被引频次




书目名称Automated Deduction - CADE-15被引频次学科排名




书目名称Automated Deduction - CADE-15年度引用




书目名称Automated Deduction - CADE-15年度引用学科排名




书目名称Automated Deduction - CADE-15读者反馈




书目名称Automated Deduction - CADE-15读者反馈学科排名

CAMP

Proving geometric theorems using clifford algebra and rewrite rules,of the previously constructed points using Clifford algebraic operators. To prove a concrete theorem, one first substitutes the expressions of the dependent points into the conclusion Clifford polynomial to obtain an expression that involves only the free points and parameters. A term-rewriting syst

Foolproof

创造性

echnic

,X.R.S: Explicit reduction systems — A first-order calculus for higher-order calculi,fined explicitly in λ. by a subsystem, called the σ.-calculus. In this paper, we use the σ⇑-calculus as the substitution mechanism of general higher-order systems which we will name .. We give general conditions to define a confluent XRS. Particularly, we restrict the general condition of orthogonal

cogent

About the confluence of equational pattern rewrite systems,13], for the case of rewriting modulo a congruence à . Huet [8]. The case we address here is rewriting using matching modulo . as done in the first-order case by Jouannaud and Kirchner [10]..The theory is then applied to the case of .-theories, for which we provided a complete unification algorithm

休战

Unification in lambda-calculi with if-then-else,der unification. Proofs of these properties are given, in particular uniqueness of the answer and the most-general-unifier property. This unification algorithm can be used to generalize first-order proofsearch algorithms to second-order logic, making possible for example a straighforward treatment o

Mumble

Etching

火海

System description: An interface between CLAM and HOL, verification, .. The interface sends HOL goals to CL.M for planning and translates plans back into HOL tactics that solve the initial goals. The project homepage can be found at http://www.cl.cam.ac.uk/Research/HVG/Clam.HOL/intro.html.