Refine
Year of publication
- 2005 (31) (remove)
Document Type
- Doctoral Thesis (31) (remove)
Language
- English (31) (remove)
Has Fulltext
- yes (31)
Keywords
- Computeralgebra (2)
- Geometric Ergodicity (2)
- Mobilfunk (2)
- air interface (2)
- Algebraic dependence of commuting elements (1)
- Algebraische Abhängigkeit der kommutierende Elementen (1)
- Algebraische Geometrie (1)
- Algorithmus (1)
- Apoptosis (1)
- Arc distance (1)
- Ascorbat (1)
- Ascorbinsäure (1)
- Ascorbylradikal (1)
- Ausfallrisiko (1)
- Automatisches Beweisverfahren (1)
- Barriers (1)
- Basisband (1)
- Blattschneiderameisen (1)
- Bottom-up (1)
- Channel estimation (1)
- Computer Algebra System (1)
- Computeralgebra System (1)
- Crash modelling (1)
- Crashmodellierung (1)
- Das Urbild von Ideal unter einen Morphismus der Algebren (1)
- Diffusionskoeffizient (1)
- Diffusionsmessung (1)
- Diffusionsmodell (1)
- Digitalmodulation (1)
- Domänenumklappen (1)
- EM algorithm (1)
- EPR (1)
- ESR (1)
- Effizienter Algorithmus (1)
- Elastizität (1)
- Elektronenspinresonanz (1)
- Eliminationsverfahren (1)
- Empfängerorientierung (1)
- Extreme Events (1)
- FPM (1)
- Feedfoward Neural Networks (1)
- Filtergesetz (1)
- Finite Elemente Methode (1)
- Finite Pointset Method (1)
- Finite-Punktmengen-Methode (1)
- Firmwertmodell (1)
- GARCH (1)
- GARCH Modelle (1)
- Gemeinsame Kanalschaetzung (1)
- Geometrische Ergodizität (1)
- Gröbner-Basis (1)
- Hidden Markov models for Financial Time Series (1)
- Homogenisierung <Mathematik> (1)
- Implementierung (1)
- Intensität (1)
- Kanalschätzung (1)
- Knuth-Bendix completion (1)
- Knuth-Bendix-Vervollständigung (1)
- Kombinatorik (1)
- Kommutative Algebra (1)
- Kontinuum <Mathematik> (1)
- Kontinuumsphysik (1)
- Kreitderivaten (1)
- Lineare Elastizitätstheorie (1)
- Luftschnittstellen (1)
- MIMO (1)
- MIMO-Antennen (1)
- Maximal Cohen-Macaulay modules (1)
- Maximale Cohen-Macaulay Moduln (1)
- Maximum Likelihood Estimation (1)
- Maximum-Likelihood-Schätzung (1)
- Mehrtraegeruebertragungsverfahren (1)
- Mikroelektronik (1)
- Modellierung (1)
- Modulationsübertragungsfunktion (1)
- Morphismus (1)
- Multileaf collimator (1)
- Nanocomposites (1)
- Navier-Stokes-Gleichung (1)
- Nekrose (1)
- Netzwerksynthese (1)
- Nichtkommutative Algebra (1)
- Nichtlineare Zeitreihenanalyse (1)
- Numerische Mathematik (1)
- OFDM (1)
- OFDM mobile radio systems (1)
- OFDM-Mobilfunksysteme (1)
- Papiermaschine (1)
- Phasengleichgewicht (1)
- Polymere (1)
- Portfoliomanagement (1)
- Poröser Stoff (1)
- Preimage of an ideal under a morphism of algebras (1)
- ROS (1)
- Ratenabhängigkeit (1)
- Reaktive Sauerstoffspezies (1)
- Redundanzvermeidung (1)
- Restricted Regions (1)
- Rhabdomyolyse (1)
- Simulation (1)
- Skelettmuskel (1)
- Software-Architektur (1)
- Spannungs-Dehn (1)
- Spherical Location Problem (1)
- Stabile Vektorbundle (1)
- Stable vector bundles (1)
- Statine (1)
- Test for Changepoint (1)
- Thermodynamik (1)
- Time Series (1)
- Tropenökologie (1)
- Upwind-Verfahren (1)
- Verbundwerkstoffe (1)
- Viskosität (1)
- Vitamin C (1)
- Vitamin C-Derivate (1)
- Wahrscheinlichkeitsfunktion (1)
- Waldfragmentierung (1)
- analoge Mikroelektronik (1)
- apoptosis (1)
- ascorbate (1)
- ascorbic acid (1)
- ascorbyl radical (1)
- automated theorem proving (1)
- beyond 3G (1)
- bottom-up (1)
- combinatorics (1)
- computeralgebra (1)
- default time (1)
- diffusion coefficient (1)
- diffusion measurement (1)
- diffusion model (1)
- domain switching (1)
- face value (1)
- finite element method (1)
- float glass (1)
- forest fragmentation (1)
- implementation (1)
- intensity (1)
- jenseits der dritten Generation (1)
- joint channel estimation (1)
- large scale integer programming (1)
- leaf-cutting ants (1)
- linear kinetics theory (1)
- lineare kinetische Theorie (1)
- mehreren Uebertragungszweigen (1)
- mixed convection (1)
- mobile radio (1)
- multi-carrier (1)
- multi-user (1)
- necrosis (1)
- network synthesis (1)
- nichtlineare Netzwerke (1)
- non-conventional (1)
- nonlinear circuits (1)
- portfolio (1)
- probabilistic approach (1)
- rate-dependency (1)
- receiver orientation (1)
- rhabdomyolysis (1)
- service area (1)
- skeletal muscle cells (1)
- statin (1)
- superposed fluids (1)
- thermodynamic model (1)
- translinear circuits (1)
- translineare Schaltungen (1)
- tropical ecology (1)
- tropical rainforest (1)
- tropischer Regenwald (1)
- viscosity model (1)
- wireless communications system (1)
Faculty / Organisational entity
- Kaiserslautern - Fachbereich Mathematik (15)
- Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik (5)
- Kaiserslautern - Fachbereich Maschinenbau und Verfahrenstechnik (5)
- Kaiserslautern - Fachbereich Chemie (4)
- Kaiserslautern - Fachbereich Biologie (1)
- Kaiserslautern - Fachbereich Informatik (1)
Automated theorem proving is a search problem and, by its undecidability, a very difficult one. The challenge in the development of a practically successful prover is the mapping of the extensively developed theory into a program that runs efficiently on a computer. Starting from a level-based system model for automated theorem provers, in this work we present different techniques that are important for the development of powerful equational theorem provers. The contributions can be divided into three areas: Architecture. We present a novel prover architecture that is based on a set-based compression scheme. With moderate additional computational costs we achieve a substantial reduction of the memory requirements. Further wins are architectural clarity, the easy provision of proof objects, and a new way to parallelize a prover which shows respectable speed-ups in practice. The compact representation paves the way to new applications of automated equational provers in the area of verification systems. Algorithms. To improve the speed of a prover we need efficient solutions for the most time-consuming sub-tasks. We demonstrate improvements of several orders of magnitude for two of the most widely used term orderings, LPO and KBO. Other important contributions are a novel generic unsatisfiability test for ordering constraints and, based on that, a sufficient ground reducibility criterion with an excellent cost-benefit ratio. Redundancy avoidance. The notion of redundancy is of central importance to justify simplifying inferences which are used to prune the search space. In our experience with unfailing completion, the usual notion of redundancy is not strong enough. In the presence of associativity and commutativity, the provers often get stuck enumerating equations that are permutations of each other. By extending and refining the proof ordering, many more equations can be shown redundant. Furthermore, our refinement of the unfailing completion approach allows us to use redundant equations for simplification without the need to consider them for generating inferences. We describe the efficient implementation of several redundancy criteria and experimentally investigate their influence on the proof search. The combination of these techniques results in a considerable improvement of the practical performance of a prover, which we demonstrate with extensive experiments for the automated theorem prover Waldmeister. The progress achieved allows the prover to solve problems that were previously out of reach. This considerably enhances the potential of the prover and opens up the way for new applications.