Combining logical and algebraic techniques for natural style proving in elementary analysis

PCS (Proving-Computing-Solving) introduced by B. Buchberger in 2001 and S-Decomposition, introduced by T. Jebelean in 2001, are strategies for handling proof problems by combining logic inference steps (e.g., modus ponens, Skolemization, instantiation) with rewriting steps (application of definitions) and solving procedures based on algebraic techniques (e.g., Groebner Bases, Cylindrical Algebraic Decomposition).

MoreLess

Year of publication:	2009
Authors:	Vajda, Robert ; Jebelean, Tudor ; Buchberger, Bruno
Published in:	Mathematics and Computers in Simulation (MATCOM). - Elsevier, ISSN 0378-4754. - Vol. 79.2009, 8, p. 2310-2316
Publisher:	Elsevier
Subject:	Automated theorem proving \| Extended quantifier elimination \| CAD \| Groebner Bases

More details

Type of publication:	Article
Source:	RePEc - Research Papers in Economics

Persistent link: https://www.econbiz.de/10010749986