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

Showing results 21 to 40 of 146.
Sorted by year (citations)

previous 1 2 3 4 ... 6 7 8 next

  1. Jaroschek, Maximilian; Dobal, Pablo Federico; Fontaine, Pascal: Adapting real quantifier elimination methods for conflict set computation (2015)
  2. Kamyar, Reza; Peet, Matthew M.: Polynomial optimization with applications to stability analysis and control -- alternatives to sum of squares (2015)
  3. Kredel, Heinz: Parametric solvable polynomial rings and applications (2015)
  4. Nikolov, Geno; Pillwein, Veronika: An extension of Turán’s inequality (2015)
  5. Samal, Satya Swarup; Grigoriev, Dima; Fröhlich, Holger; Weber, Andreas; Radulescu, Ovidiu: A geometric method for model reduction of biochemical networks with polynomial rate functions (2015)
  6. Xu, Ming; Li, Zhi-Bin; Yang, Lu: Quantifier elimination for a class of exponential polynomial formulas (2015)
  7. Anai, Hirokazu: Applied algebraic geometry in model based design for manufacturing (2014)
  8. Casagrande, A.; Dreossi, T.; Fabriková, J.; Piazza, C.: (\epsilon)-semantics computations on biological systems (2014)
  9. Chen, Changbo; Maza, Marc Moreno: An incremental algorithm for computing cylindrical algebraic decompositions (2014)
  10. Eirinakis, Pavlos; Ruggieri, Salvatore; Subramani, K.; Wojciechowski, Piotr: On quantified linear implications (2014)
  11. Hladík, Milan; Ratschan, Stefan: Efficient solution of a class of quantified constraints with quantifier prefix exists-forall (2014)
  12. Huang, Zongyan; England, Matthew; Wilson, David; Davenport, James H.; Paulson, Lawrence C.; Bridge, James: Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition (2014)
  13. Iwane, Hidenao; Yanami, Hitoshi; Anai, Hirokazu: SyNRAC: a toolbox for solving real algebraic constraints (2014)
  14. Kredel, Heinz: Comprehensive Gröbner bases in a Java computer algebra system (2014)
  15. Ruggieri, Salvatore; Eirinakis, Pavlos; Subramani, K.; Wojciechowski, Piotr: On the complexity of quantified linear systems (2014)
  16. de Moura, Leonardo; Passmore, Grant Olney: The strategy challenge in SMT solving (2013)
  17. She, Zhikun; Li, Haoyang; Xue, Bai; Zheng, Zhiming; Xia, Bican: Discovering polynomial Lyapunov functions for continuous dynamical systems (2013)
  18. Zhan, Naijun; Wang, Shuling; Zhao, Hengjun: Formal modelling, analysis and verification of hybrid systems (2013)
  19. Zhao, Hengjun; Zhan, Naijun; Kapur, Deepak: Synthesizing switching controllers for hybrid systems by generating invariants (2013)
  20. Borralleras, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: SAT modulo linear arithmetic for solving polynomial constraints (2012)

previous 1 2 3 4 ... 6 7 8 next