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 121 to 140 of 160.
Sorted by year (citations)

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

  1. Gottliebsen, Hanne; Kelsey, Tom; Martin, Ursula: Hidden verification for computational mathematics (2005)
  2. Monniaux, David: The parallel implementation of the astrée static analyzer (2005)
  3. Mysore, V.; Piazza, C.; Mishra, B.: Algorithmic algebraic model checking. II: Decidability of semi-algebraic model checking and its applications to systems biology (2005)
  4. Sofronie-Stokkermans, Viorica: Hierarchic reasoning in local theory extensions (2005)
  5. Dolzmann, Andreas; Seidl, Andreas; Sturm, Thomas: Efficient projection orders for CAD (2004)
  6. Brown, Christopher W.: QEPCAD B: A program for computing with semi-algebraic sets using CADs (2003)
  7. Colón, Michael A.; Sankaranarayanan, Sriram; Sipma, Henny B.: Linear invariant generation using non-linear constraint solving. (2003)
  8. Seidl, Andreas; Sturm, Thomas: A generic projection operator for partial cylindrical algebraic decomposition (2003)
  9. Senesky, Matthew; Eirea, Gabriel; Koo, T. John: Hybrid modelling and control of power electronics (2003)
  10. Anai, Hirokazu; Weispfenning, Volker: Reach set computations using real quantifier elimination (2002)
  11. Møller, Jesper B.: DDDLIB: A library for solving quantified difference inequalities (2002)
  12. Adams, Andrew; Dunstan, Martin; Gottliebsen, Hanne; Kelsey, Tom; Martin, Ursula; Owre, Sam: Computer algebra meets automated theorem proving: Integrating Maple and PVS (2001)
  13. Brown, Christopher W.: Simple CAD construction and its applications (2001)
  14. El Kahoui, M’hammed; Weber, Andreas; Eberhardt, Bernd: Improved algorithms for linear complementarity problem arising from collision response (2001)
  15. Ioakimidis, N. I.: Finite differences/elements in classical beam problems: Derivation of feasibility conditions under parametric inequality constraints with the help of Reduce and REDLOG (2001)
  16. Lafferriere, Gerardo; Pappas, George J.; Yovine, Sergio: Symbolic reachability computation for families of linear vector fields (2001)
  17. Mazzucco, Isolde: SYMOPT: Symbolic parametric mathematical programming (2001)
  18. Weispfenning, Volker: Semilinear motion planning in REDLOG (2001)
  19. Weispfenning, Volker: Semilinear motion planning among moving objects in REDLOG (2001)
  20. Annichini, Aurore; Asarin, Eugene; Bouajjani, Ahmed: Symbolic techniques for parametric reasoning about counter and clock systems (2000)

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