Combining algebraic computing and term-rewriting for geometry theorem proving

DOI10.1007/BFB0055909MaRDI QIDQ4217954zbMATH OpenFDO

Authors Stéphane Fèvre, Dongming Wang

Publication date 11 November 1998

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BFB0055909

zbMATH Keywords

algebraic computingautomated theorem provingClifford algebraic reductiongeometry theorem provingterm-rewriting

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Software, source code, etc. for problems pertaining to geometry (51-04) Software, source code, etc. for problems pertaining to differential geometry (53-04) Grammars and rewriting systems (68Q42) Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 1389649
• Proving geometric theorems using Clifford algebra and rewrite rules
• Clifford term rewriting for geometric reasoning in 3D
• scientific article; zbMATH DE number 2128063
• A Clifford algebraic method for geometric reasoning

Cited in

(9)

• Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
• A review and prospect of readable machine proofs for geometry theorems
• A symbolic transformation language and its application to a multiscale method
• Rewriting input expressions in complex algebraic geometry provers
• Integration of reasoning and algebraic calculus in geometry
• Proving geometric theorems using Clifford algebra and rewrite rules
• scientific article; zbMATH DE number 6984221 (Why is no real title available?)
• scientific article; zbMATH DE number 1389649 (Why is no real title available?)
• Clifford term rewriting for geometric reasoning in 3D

Describes a project that uses

Uses Software

• Maple
• OCaml

This page was built for publication: Combining algebraic computing and term-rewriting for geometry theorem proving

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4217954)