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

Robert Vajda, Tudor Jebelean and Bruno Buchberger

Mathematics and Computers in Simulation (MATCOM), 2009, vol. 79, issue 8, 2310-2316

Abstract: 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).

Keywords: Automated theorem proving; Extended quantifier elimination; CAD; Groebner Bases (search for similar items in EconPapers)
Date: 2009
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
http://www.sciencedirect.com/science/article/pii/S0378475408003741
Full text for ScienceDirect subscribers only

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:eee:matcom:v:79:y:2009:i:8:p:2310-2316

DOI: 10.1016/j.matcom.2008.11.002

Access Statistics for this article

Mathematics and Computers in Simulation (MATCOM) is currently edited by Robert Beauwens

More articles in Mathematics and Computers in Simulation (MATCOM) from Elsevier
Bibliographic data for series maintained by Catherine Liu ().