Refine
Year of publication
- 1999 (525) (remove)
Document Type
- Preprint (397)
- Article (73)
- Doctoral Thesis (28)
- Course Material (6)
- Master's Thesis (6)
- Report (5)
- Lecture (3)
- Study Thesis (3)
- Working Paper (2)
- Diploma Thesis (1)
Keywords
- Case-Based Reasoning (11)
- AG-RESY (6)
- Praktikum (6)
- Fallbasiertes Schliessen (5)
- HANDFLEX (5)
- Location Theory (5)
- PARO (5)
- case-based problem solving (5)
- Abstraction (4)
- Fallbasiertes Schließen (4)
- Knowledge Acquisition (4)
- resolution (4)
- Internet (3)
- Knowledge acquisition (3)
- Maschinelles Lernen (3)
- Multicriteria Optimization (3)
- Requirements/Specifications (3)
- case-based reasoning (3)
- distributed software development (3)
- distributed software development process (3)
- explanation-based learning (3)
- problem solving (3)
- theorem proving (3)
- Algebraic Optimization (2)
- Brillouin light scattering spectroscopy (2)
- CAPlan (2)
- Combinatorial Optimization (2)
- Deduction (2)
- Diagnose technischer Systeme (2)
- Geometrical Algorithms (2)
- KLUEDO (2)
- Kinetic Schemes (2)
- MOLTKE-Projekt (2)
- Network Protocols (2)
- PATDEX (2)
- Partial functions (2)
- SDL (2)
- Server (2)
- Software Engineering (2)
- Wannier-Stark systems (2)
- Wissensakquisition (2)
- World Wide Web (2)
- analogy (2)
- application (2)
- average density (2)
- building automation (2)
- case based reasoning (2)
- conservative extension (2)
- consistency (2)
- design patterns (2)
- entropy (2)
- fallbasiertes Schliessen (2)
- formal specification (2)
- frames (2)
- incompressible Navier-Stokes equations (2)
- lattice Boltzmann method (2)
- learning system (2)
- localization (2)
- low Mach number limit (2)
- many-valued logic (2)
- problem formulation (2)
- quantum mechanics (2)
- requirements engineering (2)
- resonances (2)
- reuse (2)
- spin wave quantization (2)
- tactics (2)
- 90° orientation (1)
- ATP-Synthase (1)
- Abelian groups (1)
- Ablagestruktur (1)
- Abstract ODE (1)
- Access System (1)
- Ad-hoc workflow (1)
- Adaption (1)
- Agents (1)
- Algebraic optimization (1)
- Alterssicherung (1)
- Analysis (1)
- Analytic semigroup (1)
- Antwortspektrenverfahren (1)
- Apoptose (1)
- Applications (1)
- Approximation (1)
- Approximation Algorithms (1)
- Automated Reasoning (1)
- Automated theorem proving (1)
- Automation (1)
- Autonomous mobile robots (1)
- Autoregression (1)
- Banach lattice (1)
- Bayes risk (1)
- Betriebsfestigkeit (1)
- Bisector (1)
- Bitlisten (1)
- Blackboard architecture (1)
- Brillouin light scattering (1)
- Brownian motion (1)
- CDK1 (1)
- CNC-Maschine (1)
- COMOKIT (1)
- Case Study (1)
- Case Study Erfahrungsdatenbank (1)
- Case-based problem solving (1)
- Causal Ordering (1)
- Causality (1)
- Chapman Enskog distributions (1)
- Chorin's projection scheme (1)
- Classification (1)
- Classification Tasks (1)
- CoMo-Kit (1)
- Collocation Method plus (1)
- Complexity and performance of numerical algorithms (1)
- Computational Fluid Dynamics (1)
- Computer Assisted Tomograp (1)
- Computer supported cooperative work (1)
- Concept mapping (1)
- Concept maps (1)
- Constraint Graphs (1)
- Contract net (1)
- Control Design Styles (1)
- Convexity (1)
- Cooperative decision making (1)
- Correlation (1)
- Cosine function (1)
- Coxeter groups (1)
- Crofton's intersection formulae (1)
- Curie temperature (1)
- DES (1)
- Damon-Eshbach spin wave modes (1)
- Datenreduktion (1)
- Decision Making (1)
- Declarative and Procedural Knowledge (1)
- Design Patterns (1)
- Design Styles (1)
- Diagnosesystem (1)
- Didaktik (1)
- Difference Reduction (1)
- Differential Cross-Sections (1)
- Diphenylfulven (1)
- Discrete decision problems (1)
- Discrete velocity models (1)
- Distributed Computation (1)
- Distributed Deb (1)
- Distributed Multimedia Applications (1)
- Distributed Software Development (1)
- Distributed Software Development Projects (1)
- Distributed System (1)
- Distributed software development support (1)
- Distributed systems (1)
- Dublin Core (1)
- Durchflußzytometrie (1)
- Dynamic capillary pressure (1)
- Dynamik (1)
- Dynasys (1)
- Dübelkennlinie (1)
- EBG (1)
- ESR-Spektroskopie (1)
- Ecommerce (1)
- Eisencarbonylkomplexe (1)
- Elastic properties (1)
- Equality reasoning (1)
- Equational Reasoning (1)
- Experience Base (1)
- Experience Database (1)
- Experiment (1)
- Experimental Data (1)
- Expertensysteme (1)
- Extensibility (1)
- F1-ATPase (1)
- Fachdidaktik (1)
- Fallstu (1)
- Farbmodell (1)
- Feature Technology (1)
- Ferromagnetism (1)
- Filter-Diagonalization (1)
- Fluktuationen der kleinen Eigenwerte des Dirac-Operators (1)
- Forbidden Regions (1)
- Frauen (1)
- Fredholm integral equation of the second kind (1)
- Fulven (1)
- Fuzzy Programming (1)
- Fünfgliedrige heterocyclische Betaine (Synthese und Reaktivität) (1)
- GPS-satellite-to-satellite tracking (1)
- Gauss-Manin connection (1)
- Gebäude (1)
- Gebäudeautomation (1)
- Generic Methods (1)
- Global Optimization (1)
- Global Predicate Detection (1)
- Global Software Highway (1)
- Global optimization (1)
- HOT (1)
- HTE (1)
- HTML (1)
- Hadwiger's recursive de nition of the Euler number (1)
- Hamiltonian groups (1)
- Hardy space (1)
- Harvest (1)
- Helmholtz decomposition (1)
- Herman-Kluk-Propagator (1)
- High frequency switching (1)
- Homogeneous Relaxation (1)
- Huffman (1)
- Huffman-Code (1)
- IDEA (1)
- INRECA (1)
- Ill-posed Problems (1)
- Improperly posed problems (1)
- Impulse control (1)
- Indigo (1)
- Indirubin (1)
- Induktive Logische Programmierung (1)
- Induktiven Logischen Programmierung (1)
- Informationstechnologie (1)
- Intelligent Agents (1)
- Intelligent agents (1)
- Interacting Magnetic Dots and Wires (1)
- Interleaved Planning (1)
- Isoindigo (1)
- Iterative Methods (1)
- Java (1)
- Jeffreys' prior (1)
- Kinetic Schems (1)
- Kinetic theory (1)
- Knuth-Bendix completion algorithm (1)
- Kogut-Susskind-Fermionen (1)
- Komprimierung (1)
- Kooperation (1)
- Kopfbolzendübel (1)
- Kryptographie (1)
- Kryptologie (1)
- Kullback Leibler distance (1)
- Lagrangian Functions (1)
- Language Constructs (1)
- Lattice Boltzmann Method (1)
- Lattice Boltzmann methods (1)
- Laufkomprimierung (1)
- Lernalgorithmen (1)
- Lexicographic Order (1)
- Lexicographic max-ordering (1)
- Linear membership function (1)
- Local completeness (1)
- Local existence uniqueness (1)
- Location theory (1)
- Logic Design (1)
- Logical Time (1)
- Logische Programmierung (1)
- MHEG (1)
- MOO (1)
- MVP-L (1)
- Map Building (1)
- Markov process (1)
- Maturity of Software Engineering (1)
- Max-Ordering (1)
- Mechanical Engineering (1)
- Metadaten (1)
- Methods (1)
- Methylphenylfulven (1)
- Mie representation (1)
- Miner-Regel (1)
- Minkowski space (1)
- Mn-Si-C alloy films (1)
- Modale Analyse (1)
- Modellbildung (1)
- Modellierung (1)
- Monte-Carlo-Simulation chiraler (1)
- Multicriteria Location (1)
- Multicriteria optimization (1)
- Multiple Criteria (1)
- Multiple Objective Programs (1)
- NMR-Spektroskopie (1)
- NP-completeness (1)
- Navier-Stokes equations (1)
- Nennspannungskonzept (1)
- Nonstationary processes (1)
- Numerical Simulation (1)
- Object-Relational DataBase Management Systems (ORDBMS) (1)
- Object-Relational Database Systems (1)
- Open-Source (1)
- Optimization (1)
- PATDEX 2 (1)
- Palm distribution (1)
- Palm distributions (1)
- Pareto Optimality (1)
- Pareto Points (1)
- Pauson-Khand (1)
- Photoreaktionen (1)
- Planning and Verification (1)
- Polynomial Eigenfunctions (1)
- Porous flow (1)
- Position- and Orientation Estimation (1)
- Potential transform (1)
- Problem Solvers (1)
- Process Management (1)
- Process support (1)
- Produktionsdesign (1)
- Project Management (1)
- Propenylfulven (1)
- Pullen Edmonds system (1)
- Quality Improvement Paradigm (QIP) (1)
- Quantenchromodynamik (1)
- Quantum Chaos (1)
- Quantum mechanics (1)
- RDF (1)
- RGB (1)
- RLE (1)
- RSA (1)
- RSWK (1)
- Random Errors (1)
- Random-Matrix-Theorie (1)
- Rarefied Polyatomic Gases (1)
- Rectifiability (1)
- Regionalplan (1)
- Repositories (1)
- Requirements engineering (1)
- Resonant tunneling diode (1)
- Resource Description Framework (1)
- Reuse (1)
- SDL-oriented Object Modeling Technique (1)
- SDL-pattern a (1)
- SKALP (1)
- SOMT (1)
- SQUID magnetometry (1)
- SUc(2)-Eichfelder (1)
- SWB (1)
- Saddle Points (1)
- Sandercock-type multipath tandem Fabry-Perot interferometer (1)
- Sandwichkomplex (1)
- Scalar type operator (1)
- Schalenbauweise (1)
- Schalenelement (1)
- Schlagwortkatalogisierung (1)
- Self-Referencing (1)
- Semantics of Programming Languages (1)
- Semiklassik (1)
- Shannon capacity (1)
- Shannon optimal priors (1)
- Shock Wave Problem (1)
- Similarity Assessment (1)
- Simulation (1)
- Smalltalk (1)
- Software Agents (1)
- Software development (1)
- Software development environment (1)
- Software engineering (1)
- Spatial Binary Images (1)
- Spectral Analysis (1)
- Spindynamik (1)
- Square-mean Convergence (1)
- Stark systems (1)
- Stoner-like magnetic particles (1)
- Structural Adaptation (1)
- Structure (1)
- Structuring Approach (1)
- Struktur-Wirkungs-Abhängigkeit (1)
- Synthese (1)
- Systemarchitektur (1)
- Tactics (1)
- Term rewriting systems (1)
- Tetraphosphabicyclobutan (1)
- Theorem of Plemelj-Privalov (1)
- Topology Preserving Networks (1)
- Translation planes (1)
- Triangular fuzzy number (1)
- Typologie (1)
- Undecaphosphor (1)
- Unterricht (1)
- Vector Time (1)
- Vector-valued holomorphic function (1)
- Verschlüsselung (1)
- Vetor optimization (1)
- Vigenere (1)
- Virtual Corporation (1)
- Virtual Software Projects (1)
- Voronoi diagram (1)
- Wannier-Bloch states (1)
- Wide Area Multimedia Group Interaction (1)
- Wissenserwerb (1)
- Word problem (1)
- Workflow Replication (1)
- World-Wide Web (1)
- Wöhlerlinie (1)
- Zeitfestigkeit (1)
- Zellzyklus (1)
- Zugriffstruktur (1)
- Zugriffsystem (1)
- abgeschlossene Population (1)
- abstract description (1)
- adaption (1)
- alpha (1)
- analogical reasoning (1)
- anisotropic coupling between magnetic i (1)
- anisotropic coupling mechanism (1)
- approximation methods (1)
- arbitrary function (1)
- arrays of magnetic dots and wires (1)
- artificial intelligence (1)
- assembly sequence design (1)
- automated code generation (1)
- automated computer learning (1)
- automated synchronization (1)
- autonomes Lernen (1)
- autonomous learning (1)
- average densities (1)
- bcc-Fe(001) (1)
- beta-ungesättigte Aldehyde und Ketone (1)
- bicriterion path problems (1)
- bipolar quantum drift diffusion model (1)
- biquadratic interlayer coupling (1)
- bootstrap (1)
- brillouin light scattering (1)
- business process modelling (1)
- cancer (1)
- case-based planner (1)
- case-based planning (1)
- cash management (1)
- cdc2 (1)
- center hyperplane (1)
- centrally symmetric polytope (1)
- chaotic dynamics (1)
- co-learning (1)
- coherent-state-propagator (1)
- combined systems with sha (1)
- common transversal (1)
- communication architectures (1)
- communication protocols (1)
- communication subsystem (1)
- compilation (1)
- complete presentations (1)
- completeness (1)
- complex energ (1)
- complex energy resonances (1)
- comprehensive reuse (1)
- compressible Navier Stokes equations (1)
- computer aided planning (1)
- computer control (1)
- computer-supported cooperative work (1)
- concept representation (1)
- conceptual representation (1)
- concurrent software (1)
- confluence (1)
- constraint satisfaction problem (CSP) (1)
- continuous media (1)
- convex distance funtion (1)
- convex operator (1)
- cooperative problem solving (1)
- critical thickness (1)
- cross-correlation (1)
- customization of communication protocols (1)
- cyclinabhängige Kinasen (1)
- decision support (1)
- decisions (1)
- decrease direction (1)
- deficiency (1)
- density distribution (1)
- dependency management (1)
- deposition temperature (1)
- design processes (1)
- diagnostic problems (1)
- dipole-exchange surface (1)
- direct product (1)
- directional derivative (1)
- discrete element method (1)
- discrete equilibrium distributions (1)
- discrete velocity models (1)
- discretization (1)
- disjoint union (1)
- distributed (1)
- distributed c (1)
- distributed deduction (1)
- distributed document management (1)
- distributed enterprise (1)
- distributed groupware environment (1)
- distributed multi-platform software development (1)
- distributed multi-platform software development projects (1)
- distributed software configuration management (1)
- distributed softwaredevelopment tools (1)
- dynamical systems (1)
- dynamische Systeme (1)
- enhanced coercivity (1)
- epitaxial growth (1)
- evolutionary spectrum (1)
- exchange coupling (1)
- exchange rate (1)
- exchange-bias bilayer Fe/MnPd (1)
- exchange-coupled rare-earth (1)
- experience base (1)
- experimental software engineering (1)
- exponential rate (1)
- f-dissimilarity (1)
- fallbasiertes planen (1)
- final prediction error (1)
- finite difference method (1)
- flexible workflows (1)
- flüssigkristalliner Phasen (1)
- formal description techniques (1)
- formal reasoning (1)
- formulation as integral equation (1)
- frequency splitting betwe (1)
- function of bounded variation (1)
- gauge (1)
- general multidimensional moment problem (1)
- generalized Gummel itera (1)
- generic design of a customized communication subsystem (1)
- geodetic (1)
- geomagnetic field modelling from MAGSAT data (1)
- geometric measure theory (1)
- geometrical algorithms (1)
- geopotential determination (1)
- global optimization (1)
- goal oriented completion (1)
- granular flow (1)
- growth optimal portfolios (1)
- harmonic WFT (1)
- head-on collisions (1)
- heterogeneous large-scale distributed DBMS (1)
- high-level caching of potentially shared networked documents (1)
- higher order logic (1)
- higher-order anisotropies (1)
- higher-order tableaux calculus (1)
- higher-order theorem prover (1)
- homological algebra (1)
- hybrid knowledge representation (1)
- hyperbolic systems of conservation laws (1)
- hyperplane transversal (1)
- industrial supervision (1)
- inelastic light scattering (1)
- information (1)
- information systems engineering (1)
- innermost termination (1)
- instanton method (1)
- intelligent agents (1)
- interaktiv (1)
- interest oriented portfolios (1)
- internal approximation (1)
- internet event synchronizer (1)
- intersection local time (1)
- inverse Fourier transform (1)
- inverse mathematical models (1)
- isochronous streams (1)
- knowledge space (1)
- knowledge-based planning (1)
- konzeptuelle Modelierung (1)
- lacunarity distribution (1)
- large deviations (1)
- layered magnetic systems (1)
- learning (1)
- learning algorithms (1)
- level splitting (1)
- lifetime statistics (1)
- lifetimes (1)
- linked abstraction workflows (1)
- locally maximal clone (1)
- locally stationary process (1)
- location (1)
- location problem (1)
- logarithmic average (1)
- logarithmic utility (1)
- macroscopic quantum coherence (1)
- magnetic Ni80Fe20 wires (1)
- magnetische Vielfachschichten (1)
- magnetization reversal process (1)
- magneto-optical Kerr effect (1)
- magnetostatic surface spin waves (1)
- martingale measu (1)
- mathematical concept (1)
- maximum-entropy (1)
- metastable Pd(001) (1)
- middleware (1)
- minimal paths (1)
- minimax rate (1)
- minimax risk (1)
- mobile agents (1)
- mobile agents approach (1)
- modelling time (1)
- modularity (1)
- moment realizability (1)
- monitoring and managing distributed development processes (1)
- monodromy (1)
- morphism (1)
- motion planning (1)
- multi-agent architecture (1)
- multicriteria minimal path problem is presented (1)
- multicriteria optimization (1)
- multidimensional Kohonen algorithm (1)
- multimedia (1)
- multiple objective linear programming problem (1)
- multiple-view product modeling (1)
- multiresolution analysis (1)
- narrowing (1)
- negotiation (1)
- neural networks (1)
- non-convex optimization (1)
- noninformative prior (1)
- nonlinear thresholding (1)
- nonlinear wavelet thresholding (1)
- norm (1)
- normal cone (1)
- numeraire portfolios (1)
- numerical computation (1)
- object frameworks (1)
- objektimmanente Kriterien (1)
- order selection (1)
- order-sorted logic (1)
- order-two densities (1)
- order-two density (1)
- ovoids (1)
- paramodulation (1)
- patterned magnetic permalloy films (1)
- phase space (1)
- phase-space (1)
- plan enactment (1)
- polyhedral norm (1)
- portfolio optimisation (1)
- preservation of relations (1)
- problem solvers (1)
- process model (1)
- process modelling (1)
- process support system (PROSYT) (1)
- process-centred environments (1)
- profiles (1)
- programmable client-server systems (1)
- project coordination (1)
- projected quasi-gradient method (1)
- proof plans (1)
- protocol (1)
- pseudo-compressibility method (1)
- qauntum mechanis (1)
- quadratic forms (1)
- quasi-one-dimensional spin wave envelope solitons (1)
- quasienergy (1)
- radiation therapy (1)
- rate control (1)
- reactive systems (1)
- real time (1)
- real-time (1)
- real-time temporal logic (1)
- receptive safety properties (1)
- reference prior (1)
- regularization by wavelets (1)
- rela (1)
- reliability (1)
- requirements (1)
- reuse repositories (1)
- robustness (1)
- scaled translates (1)
- search algorithms (1)
- second order logic (1)
- semiklassische Methoden (1)
- semiklassische Propagatoren (1)
- shape aniso-tropies (1)
- shear flow (1)
- short magnetic fieldpulses (1)
- short-time periodogram (1)
- shortest sequence (1)
- similarity measure (1)
- single domain uniaxial magnetic particles (1)
- singularities (1)
- software agents (1)
- software project (1)
- software project management (1)
- sorted logic (1)
- soundness (1)
- spectral sequences (1)
- spin wave excitations (1)
- spinwaves (1)
- squares (1)
- statistical experiment (1)
- stochastic stability (1)
- structured permalloy films (1)
- switching properties (1)
- system behaviour (1)
- tableau (1)
- tangent measure distributions (1)
- temperature dependence (1)
- temporal logic (1)
- termination (1)
- theorem prover (1)
- thin h-BN films (1)
- time series (1)
- time-varying autoregression (1)
- topology preserving maps (1)
- traceability (1)
- transition rates (1)
- transition-metal (1)
- translation (1)
- transverse bias field (1)
- traveling salesman problem (1)
- treatment planning (1)
- trial systems (1)
- triple layer stacks (1)
- two-dimensional self-focused spin wave packets (1)
- typical examples (1)
- typical instance (1)
- uncertainty principle (1)
- uniform ergodicity (1)
- uniqueness (1)
- value preserving portfolios (1)
- vector measure (1)
- vector wavelets (1)
- verlustfrei (1)
- virtual market place (1)
- viscosity solutions (1)
- visual process modelling environment (1)
- wall energy (1)
- wall thickness (1)
- wavelet estimators (1)
- wavelet transform (1)
- weak termination (1)
- windowed Fourier transform (1)
- wissensbasierte Systeme (1)
- wissensbasierter Systeme der Arbeitsplanerstellung (1)
- work coordination (1)
- yttrium-iron garnet (YIG) fi (1)
- Örtliches Konzept (1)
- ästhetische Differenz (1)
Faculty / Organisational entity
- Kaiserslautern - Fachbereich Informatik (267)
- Kaiserslautern - Fachbereich Mathematik (131)
- Kaiserslautern - Fachbereich Physik (76)
- Kaiserslautern - Fachbereich Chemie (19)
- Kaiserslautern - Fachbereich Elektrotechnik und Informationstechnik (10)
- Fraunhofer (ITWM) (6)
- Kaiserslautern - Fachbereich ARUBI (6)
- Kaiserslautern - Fachbereich Wirtschaftswissenschaften (5)
- Kaiserslautern - Fachbereich Biologie (2)
- Kaiserslautern - Fachbereich Maschinenbau und Verfahrenstechnik (2)
- Universitätsbibliothek (1)
Mechanised reasoning systems and computer algebra systems have apparentlydifferent objectives. Their integration is, however, highly desirable, since in manyformal proofs both of the two different tasks, proving and calculating, have to beperformed. Even more importantly, proof and computation are often interwoven andnot easily separable. In the context of producing reliable proofs, the question howto ensure correctness when integrating a computer algebra system into a mechanisedreasoning system is crucial. In this contribution, we discuss the correctness prob-lems that arise from such an integration and advocate an approach in which thecalculations of the computer algebra system are checked at the calculus level of themechanised reasoning system. This can be achieved by adding a verbose mode to thecomputer algebra system which produces high-level protocol information that can beprocessed by an interface to derive proof plans. Such a proof plan in turn can beexpanded to proofs at different levels of abstraction, so the approach is well-suited forproducing a high-level verbalised explication as well as for a low-level machine check-able calculus-level proof. We present an implementation of our ideas and exemplifythem using an automatically solved extended example.
We propose a specification language for the formalization of data types with par-tial or non-terminating operations as part of a rewrite-based logical frameworkfor inductive theorem proving. The language requires constructors for designat-ing data items and admits positive/negative conditional equations as axioms inspecifications. The (total algebra) semantics for such specifications is based onso-called data models. We present admissibility conditions that guarantee theunique existence of a distinguished data model with properties similar to thoseof the initial model of a usual equational specification. Since admissibility of aspecification requires confluence of the induced rewrite relation, we provide aneffectively testable confluence criterion which does not presuppose termination.
To prove difficult theorems in a mathematical field requires substantial know-ledge of that field. In this paper a frame-based knowledge representation formalismis presented, which supports a conceptual representation and to a large extent guar-antees the consistency of the built-up knowledge bases. We define a semantics ofthe representation by giving a translation into the underlaying logic.
The amount of user interaction is the prime cause of costs in interactiveprogram verification. This paper describes an internal analogy techniquethat reuses subproofs in the verification of state-based specifications. Itidentifies common patterns of subproofs and their justifications in orderto reuse these subproofs; thus significant savings on the number of userinteractions in a verification proof are achievable.
We present an empirical study of mathematical proofs by diagonalization, the aim istheir mechanization based on proof planning techniques. We show that these proofs canbe constructed according to a strategy that (i) finds an indexing relation, (ii) constructsa diagonal element, and (iii) makes the implicit contradiction of the diagonal elementexplicit. Moreover we suggest how diagonal elements can be represented.
The problem of providing connectivity for a collection of applications is largely one of data integration: the communicating parties must agree on thesemantics and syntax of the data being exchanged. In earlier papers [#!mp:jsc1!#,#!sg:BSG1!#], it was proposed that dictionaries of definitions foroperators, functions, and symbolic constants can effectively address the problem of semantic data integration. In this paper we extend that earlier work todiscuss the important issues in data integration at the syntactic level and propose a set of solutions that are both general, supporting a wide range of dataobjects with typing information, and efficient, supporting fast transmission and parsing.
Chains of Recurrences (CRs) are a tool for expediting the evaluation of elementary expressions over regular grids. CR based evaluations of elementaryexpressions consist of 3 major stages: CR construction, simplification, and evaluation. This paper addresses CR simplifications. The goal of CRsimplifications is to manipulate a CR such that the resulting expression is more efficiently to evaluate. We develop CR simplification strategies which takethe computational context of CR evaluations into account. Realizing that it is infeasible to always optimally simplify a CR expression, we give heuristicstrategies which, in most cases, result in a optimal, or close-to-optimal expressions. The motivations behind our proposed strategies are discussed and theresults are illustrated by various examples.
Algorithms in Singular
(1999)
Top-down and bottom-up theorem proving approaches have each specific ad-vantages and disadvantages. Bottom-up provers profit from strong redundancycontrol and suffer from the lack of goal-orientation, whereas top-down provers aregoal-oriented but have weak calculi when their proof lengths are considered. Inorder to integrate both approaches our method is to achieve cooperation betweena top-down and a bottom-up prover: The top-down prover generates subgoalclauses, then they are processed by a bottom-up prover. We discuss theoreticaspects of this methodology and we introduce techniques for a relevancy-basedfiltering of generated subgoal clauses. Experiments with a model eliminationand a superposition-based prover reveal the high potential of our cooperation approach.The author was supported by the Deutsche Forschungsgemeinschaft (DFG).
We examine an approach for demand-driven cooperative theorem proving.We briefly point out the problems arising from the use of common success-driven cooperation methods, and we propose the application of our approachof requirement-based cooperative theorem proving. This approach allows for abetter orientation on current needs of provers in comparison with conventional co-operation concepts. We introduce an abstract framework for requirement-basedcooperation and describe two instantiations of it: Requirement-based exchangeof facts and sub-problem division and transfer via requests. Finally, we reporton experimental studies conducted in the areas superposition and unfailing com-pletion.The author was supported by the Deutsche Forschungsgemeinschaft (DFG).
HOT is an automated higher-order theorem prover based on HTE, an extensional higher-order tableaux calculus (Kohlhase 95). The first part of the paper introduces a variant of the calculus which closely corresponds to the proof procedure implemented in HOT. The second part discusses HOT's design that can be characterized as a concurrent Blackboard architecture. We show the usefulness of the implementation by including benchmark results for over one hundred solved problems from logic and set theory.
Orderings on polynomial interpretations of operators represent a powerful technique for proving thetermination of rewriting systems. One of the main problems of polynomial orderings concerns thechoice of the right interpretation for a given rewriting system. It is very difficult to develop techniquesfor solving this problem. Here, we present three new heuristic approaches: (i) guidelines for dealingwith special classes of rewriting systems, (ii) an algorithm for choosing appropriate special polynomialsas well as (iii) an extension of the original polynomial ordering which supports the generation ofsuitable interpretations. All these heuristics will be applied to examples in order to illustrate theirpractical relevance.
We study families V of curves in P2(C) of degree d having exactly r singular points of given topological or analytic types. We derive new sufficient conditions for V to be T-smooth (smooth of the expected dimension), respectively to be irreducible. For T-smoothness these conditions involve new invariants of curve singularities and are conjectured to be asymptotically proper, i.e., optimal up to a constant factor. To obtain the results, we study the Castelnuovo function, prove the irreducibility of the Hilbert scheme of zero-dimensional schemes associated to a cluster of infinitely near points of the singularities and deduce new vanishing theorems for ideal sheaves of zero-dimensional schemes in P2. Moreover, we give a series of examples of cuspidal curves where the family V is reducible, but where ss1(P2nC) coincides (and is abelian) for all C 2 V .
After the notion of Gröbner bases and an algorithm for constructing them was introduced by Buchberger [Bu1, Bu2] algebraic geometers have used Gröbner bases as the main computational tool for many years, either to prove a theorem or to disprove a conjecture or just to experiment with examples in order to obtain a feeling about the structure of an algebraic variety. Nontrivial problems coming either from logic, mathematics or applications usually lead to nontrivial Gröbner basis computations, which is the reason why several improvements have been provided by many people and have been implemented in general purpose systems like Axiom, Maple, Mathematica, Reduce, etc., and systems specialized for use in algebraic geometry and commutative algebra like CoCoA, Macaulay and Singular. The present paper starts with an introduction to some concepts of algebraic geometry which should be understood by people with (almost) no knowledge in this field. In the second chapter we introduce standard bases (generalization of Gr"obner bases to non-well-orderings), which are needed for applications to local algebraic geometry (singularity theory), and a method for computing syzygies and free resolutions. The last chapter describes a new algorithm for computing the normalization of a reduced affine ring and gives an elementary introduction to singularity theory. Then we describe algorithms, using standard bases, to compute infinitesimal deformations and obstructions, which are basic for the deformation theory of isolated singularities. It is impossible to list all papers where Gr"obner bases have been used in local and global algebraic geometry, and even more impossible to give an overview about these contributions. We have, therefore, included only references to papers mentioned in this tutorial paper. The interested reader will find many more in the other contributions of this volume and in the literature cited there.
Algorithmic ideal theory
(1999)
Algebraic geometers have used Gröbner bases as the main computational tool for many years, either to prove a theorem or to disprove a conjecture or just to experiment with examples in order to obtain a feeling about the structure of an algebraic variety. Non-trivial mathematical problems usually lead to non-trivial Gröbner basis computations, which is the reason why several improvements and efficient implementations have been provided by algebraic geometers (for example, the systems CoCoA, Macaulay and SINGULAR). The present paper starts with an introduction to some concepts of algebraic geometry which should be understood by people with (almost) no knowledge in this field. In the second chapter we introduce standard bases (generalization of Gröbner bases to non-well-orderings), which are needed for applications to local algebraic geometry (singularity theory), and a method for computing syzygies and free resolutions. In the third chapter several algorithms for primary decomposition of polynomial ideals are presented, together with a discussion of improvements and preferable choices. We also describe a newly invented algorithm for computing the normalization of a reduced affine ring. The last chapter gives an elementary introduction to singularity theory and then describes algorithms, using standard bases, to compute infinitesimal deformations and obstructions, which are basic for the deformation theory of isolated singularities. It is impossible to list all papers where Gröbner basis have been used in local and global algebraic geometry, and even more impossible to give an overview about these contributions. We have, therefore, included only a few references to papers which contain interesting applications and which are not mentioned in this tutorial paper. The interested reader will find many more in the other contributions of this volume and in the literature cited there.
Singular algebraic curves, their existence, deformation, families (from the local and global point of view) attract continuous attention of algebraic geometers since the last century. The aim of our paper is to give an account of results, new trends and bibliography related to the geometry of equisingular families of algebraic curves on smooth algebraic surfaces over an algebraically closed field of characteristic zero. This theory is founded in basic works of Plücker, Severi, Segre, Zariski, and has tight links and finds important applications in singularity theory, topology of complex algebraic curves and surfaces, and in real algebraic geometry.
If \(A\) generates a bounded cosine function on a Banach space \(X\) then the negative square root \(B\) of \(A\) generates a holomorphic semigroup, and this semigroup is the conjugate potential transform of the cosine function. This connection is studied in detail, and it is used for a characterization of cosine function generators in terms of growth conditions on the semigroup generated by \(B\). This characterization relies on new results on the inversion of the vector-valued conjugate potential transform.
Let \(X\) be a Banach lattice. Necessary and sufficient conditions for a linear operator \(A:D(A) \to X\), \(D(A)\subseteq X\), to be of positive \(C^0\)-scalar type are given. In addition, the question is discussed which conditions on the Banach lattice imply that every operator of positive \(C^0\)-scalar type is necessarily of positive scalar type.
We consider regularizing iterative procedures for ill-possed problems with random and nonrandom additive errors. The rate of square-mean convergence for iterative procedures with random errors is studied. The comparison theorem is established for the convergence of procedures with and without additive errors.
Vigenere-Verschlüsselung
(1999)