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 148 articles , 1 standard article )

Showing results 1 to 20 of 148.
Sorted by year (citations)

1 2 3 ... 6 7 8 next

  1. Hong, Hoon; Sturm, Thomas: Positive solutions of systems of signed parametric polynomial inequalities (2018)
  2. Röbenack, Klaus; Voßwinkel, Rick; Richter, Hendrik: Automatic generation of bounds for polynomial systems with application to the Lorenz system (2018)
  3. Roux, Pierre; Voronin, Yuen-Lam; Sankaranarayanan, Sriram: Validating numerical semidefinite programming solvers for polynomial invariants (2018)
  4. England, Matthew; Errami, Hassan; Grigoriev, Dima; Radulescu, Ovidiu; Sturm, Thomas; Weber, Andreas: Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks (2017)
  5. Kuijpers, Bart; Moelans, Bart: On the realisability of double-cross matrices by polylines in the plane (2017)
  6. Sturm, Thomas: A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications (2017)
  7. Wojciechowski, Piotr; Eirinakis, Pavlos; Subramani, K.: Analyzing restricted fragments of the theory of linear arithmetic (2017)
  8. Wojciechowski, Piotr; Eirinakis, Pavlos; Subramani, K.: Erratum to: “Analyzing restricted fragments of the theory of linear arithmetic” (2017)
  9. Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas: \textsfSC(^2): satisfiability checking meets symbolic computation. (Project paper) (2016)
  10. Dixit, Atul; Moll, Victor H.; Pillwein, Veronika: A hypergeometric inequality (2016)
  11. Eraşcu, Mădălina: Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms (2016)
  12. Eraşcu, Mădălina; Hong, Hoon: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation) (2016)
  13. Fukasaku, Ryoya; Iwane, Hidenao; Sato, Yosuke: On the implementation of CGS real QE (2016)
  14. Košta, Marek; Sturm, Thomas; Dolzmann, Andreas: Better answers to real questions (2016)
  15. Sankaranarayanan, Sriram: Change-of-bases abstractions for non-linear hybrid systems (2016)
  16. Uijlen, Sander; Westerbaan, Bas: A Kochen-Specker system has at least 22 vectors (2016)
  17. Xu, Ming; Zhang, Lijun; Jansen, David N.; Zhu, Huibiao; Yang, Zongyuan: Multiphase until formulas over Markov reward models: an algebraic approach (2016)
  18. Abraham, Erika: Building bridges between symbolic computation and satisfiability checking (2015)
  19. Errami, Hassan; Eiswirth, Markus; Grigoriev, Dima; Seiler, Werner M.; Sturm, Thomas; Weber, Andreas: Detection of Hopf bifurcations in chemical reaction networks using convex coordinates (2015)
  20. Fukasaku, Ryoya; Iwane, Hidenao; Sato, Yosuke: Real quantifier elimination by computation of comprehensive Gröbner systems (2015)

1 2 3 ... 6 7 8 next