REDLOG is a package that extends the computer algebra system REDUCE to a computer logic system, i.e., a system that provides algorithms for the symbolic manipulation of first-order formulas over some temporarily fixed language and theory. In contrast to theorem provers, the methods applied know about the underlying algebraic theory and make use of it. We illustrate some applications of REDLOG, describe its functionality as it appears to the user, and explain the design issues and implementation techniques.

References in zbMATH (referenced in 160 articles , 1 standard article )

Showing results 101 to 120 of 160.
Sorted by year (citations)
  1. Dolzmann, Andreas; Weispfenning, Volker: Multiple object semilinear motion planning (2007)
  2. Jacobs, Swen; Sofronie-Stokkermans, Viorica: Applications of hierarchical reasoning in the verification of complex systems (2007)
  3. Kaliszyk, Cezary; Wiedijk, Freek: Certified computer algebra on top of an interactive theorem prover (2007)
  4. Lasaruk, Aless; Sturm, Thomas: Weak quantifier elimination for the full linear theory of the integers (2007)
  5. Lasaruk, Aless; Sturm, Thomas: Weak integer quantifier elimination beyond the linear case (2007)
  6. Liska, Richard; Váchal, Pavel: Quantifier elimination supported proofs in the numerical treatment of fluid flows (2007)
  7. Mahboubi, Assia: Implementing the cylindrical algebraic decomposition within the Coq system (2007)
  8. Mysore, Venkatesh; Mishra, Bud: Algorithmic algebraic model checking. IV: Characterization of metabolic networks (2007)
  9. Nabeshima, Katsusuke: A speed-up of the algorithm for computing comprehensive Gröbner systems (2007)
  10. Pang, Y.; Spathopoulos, M. P.; Xia, Hao: Reachability and optimal control for linear hybrid automata: A quantifier elimination approach (2007)
  11. Sofronie-Stokkermans, Viorica: Hierarchical and modular reasoning in complex theories: The case of local theory extensions (2007)
  12. Suzuki, Akira; Sato, Yosuke: Implementation of CGS and CGB on Risa/Asir and other computer algebra systems using Suzuki-Sato algorithm (2007) ioport
  13. Yang, Lu; Feng, Yong; Yao, Yong: A class of mechanically decidable problems beyond Tarski’s model (2007)
  14. Brown, Christopher W.; El Kahoui, M’hammed; Novotni, Dominik; Weber, Andreas: Algorithmic methods for investigating equilibria in epidemic modeling (2006)
  15. Brown, Christopher W.; Gross, Christian: Efficient preprocessing methods for quantifier elimination (2006)
  16. Größlinger, Armin; Griebl, Martin; Lengauer, Christian: Quantifier elimination in automatic loop parallelization (2006)
  17. Kapur, Deepak: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs (2006)
  18. Sturm, Thomas: New domains for applied quantifier elimination. (Plenary talk) (2006)
  19. Suzuki, Akira; Sato, Yosuke: A simple algorithm to compute comprehensive Gröbner bases using Gröbner bases (2006)
  20. Anderson, Hugh; Khoo, Siau-Cheng; Andrei, Stefan; Luca, Beatrice: Calculating polynomial runtime properties (2005)