Implementing field extensions of the form Q[sqrt(b)]

MaRDI QIDQ7361312FDO

Authors René Thiemann

Publication date 6 February 2014

Cites work

• A Monotonic Higher-Order Semantic Path Ordering
• An Efficient Unification Algorithm
• Approximations for strategies and termination
• Arctic Termination ...Below Zero
• Artificial Intelligence and Symbolic Computation
• Automated Reasoning
• Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
• Automated Termination Analysis for Logic Programs by Term Rewriting
• Automatic termination proofs with transformation orderings
• Automating the dependency pair method
• Certification of Automated Termination Proofs
• Certification of Termination Proofs Using CeTA
• Certifying a Termination Criterion Based on Graphs, without Graphs
• Code generation via higher-order rewrite systems
• Comparing curried and uncurried rewriting
• Counterexamples to termination for the direct sum of term rewriting systems
• Data refinement in Isabelle/HOL
• Deciding Innermost Loops
• Definitional interpreters for higher-order programming languages
• Detecting Non-termination of Term Rewriting Systems Using an Unfolding Operator
• Formalizing bounded increase
• From Outermost Termination to Innermost Termination
• Frontiers of Combining Systems
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication
• Improved matrix interpretation
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Light-weight containers for Isabelle: efficient, extensible, nestable
• Logic for Programming, Artificial Intelligence, and Reasoning
• Logic Programming
• Loop detection in term rewriting using the eliminating unfoldings
• Mathematical Foundations of Computer Science 2003
• Matrix interpretations for proving termination of term rewriting
• Maximal Termination
• Mechanizing and improving dependency pairs
• Modular and incremental automated termination proofs
• Modular termination proofs for rewriting using dependency pairs
• Non-Looping String Rewriting
• On Proving Uniform Termination and Restricted Termination of Rewriting Systems
• On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting
• Overlap closures do not suffice for termination of general term rewriting systems
• Polynomials over the reals in proofs of termination : from theory to practice
• Rewriting Techniques and Applications
• Rewriting Techniques and Applications
• Satisfiability of non-linear (ir)rational arithmetic
• Semi-unification
• Term Rewriting and Applications
• Termination Analysis of Logic Programs Based on Dependency Graphs
• Termination of logic programs: Transformational methods revisited
• Termination of rewriting
• Termination of string rewriting proved automatically
• Termination of term rewriting using dependency pairs
• Transformation techniques for context-sensitive rewrite systems
• Tyrolean termination tool: techniques and features
• Verification of Erlang processes by dependency pairs
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture

Cited in

(2)

• Complex Bounded Operators
• QR Decomposition

This page was built for software: Implementing field extensions of the form Q[sqrt(b)]