bluuebunny/crossref_metadata_2025 huggingface dataset:
New Downhole-Fluid-Analysis Tool for Improved Reservoir Characterization
Authors: Dong C. , O'Keefe M. D. , Elshahawi H. , Hashem M. , Williams S. , Stensland D. , Hegeman P. , Vasques R. , Terabayashi T. , Mullins O. , Donzier E.
Published: January 2009

Downhole fluid analysis (DFA) has emerged as a key technique for characterizing the distribution of reservoir-fluid properties and determining zonal connectivity across the reservoir. Information from profiling the reservoir fluids enables sealing barriers to be proved and compositional grading to be quantified; this information cannot be obtained from conventional wireline logs. The DFA technique has been based largely on optical spectroscopy, which can provide estimates of filtrate contamination, gas/oil ratio (GOR), pH of formation water, and a hydrocarbon composition in four groups: methane (C1), ethane to pentane (C2–5), hexane and heavier hydrocarbons (C6+), and carbon dioxide (CO2). For single-phase assurance, it is possible to detect gas liberation (bubblepoint) or liquid dropout (dewpoint) while pumping reservoir fluid to the wellbore, before filling a sample bottle.

In this paper, a new DFA tool is introduced that substantially increases the accuracy of these measurements. The tool uses a grating spectrometer in combination with a filter-array spectrometer. The range of compositional information is extended from four groups to five groups: C1, ethane (C2), propane to pentane (C3–5), C6+, and CO2. These spectrometers, together with improved compositional algorithms, now make possible a quantitative analysis of reservoir fluid with greater accuracy and repeatability. This accuracy enables comparison of fluid properties between wells for the first time, thus extending the application of fluid profiling from a single-well to a multiwall basis. Field-based fluid characterization is now possible.

In addition, a new measurement is introduced—in-situ density of reservoir fluid. Measuring this property downhole at reservoir conditions of pressure and temperature provides important advantages over surface measurements. The density sensor is combined in a package that includes the optical spectrometers and measurements of fluid resistivity, pressure, temperature, and fluorescence that all play a vital role in determining the exact nature of the reservoir fluid.

Extensive tests at a pressure/volume/temperature (PVT) laboratory are presented to illustrate sensor response in a large number of live-fluid samples. These tests of known fluid compositions were conducted under pressurized and heated conditions to simulate reservoir conditions. In addition, several field examples are presented to illustrate applicability in different environments.
Potato Yield and Quality Response to Subsoil Tillage and Compaction
Authors: Copas Michael E. , Bussan Alvin J. , Drilias Michael J. , Wolkowski Richard P.
Published: January 2009

Compacted soils have been found in intensively cultivated vegetable crop regions of Central Wisconsin, resulting in the wide scale use of subsoil tillage by growers. The goal of this project was to assess potato (Solanum tuberosum L.) yield and quality response to soil compaction and subsoil tillage. Potato quality factors evaluated were marketable yield, tuber size distribution, internal quality, and sugar concentration. A controlled small plot experiment and several field scale experiments located in collaborating grower fields were conducted to assess potato and soil responses to subsoil tillage. Cone index profiles showed the potential for limited root growth below the compacted soil layer with values >2.0 MPa. Subsoil tillage reduced cone index values to <1.0 MPa below 33 cm in 2 of 3 yr. Total and U.S. no. 1 yields were not influenced by subsoil tillage. Likewise, no consistent differences were seen in the size distributions of U.S. no. 1 tubers across treatments, but subsoil tillage tended to decrease proportion of tubers 113 to 170 g. Subsoil tillage did not affect tuber glucose or sucrose concentrations at harvest or following storage for 120 d. Internal tuber defects were not affected by either compaction or subsoil tillage. The lack of consistent effects of subsoil tillage on potato yield raises questions regarding the validity of this practice. The recommendation that potato growers use subsoil tillage may be linked to increased tuber size distribution or factors other than yield such as water, nutrient, or disease management.
Effect of Irrigation with Secondary Treated Effluent on Essential Oil, Antioxidant Activity, and Phenolic Compounds in Oregano and Rosemary
Authors: Bernstein Nirit , Chaimovitch David , Dudai Nativ
Published: January 2009

Shortage of water throughout the world dictates utilization of marginal water for irrigation. Treated urban wastewater is a common alternative water source for irrigation in arid and semiarid regions. In this study we aimed to evaluate the effect of irrigation with secondary‐treated effluent on plant development, essential oil yield, antioxidant activity and selected antioxidant phenolic compounds in two commercial cultivars of the aromatic species, oregano (Origanum vulgare L.) and rosemary (Rosmarinus officinalis L.). The applied treated effluent contained higher levels of Na, Cl, HCO3,−1 P, K, NH4+1, NO3−1, Ca+Mg, B, Mn, and Fe than the local potable water used as control, and were characterized by higher values of electrical conductivity (EC), pH, and sodium absorption ratio (SAR). Since effluent effects on plants can become apparent only following several years of exposure, the plants were exposed to the water treatments for 3 yr. Despite the differences in water quality, the effluent did not affect yield quantity and quality in either crop. Plant morphological development, biomass production, percent dry leaves of the total biomass, quantity and composition of the essential oil produced, antioxidant activity, and contents of selected antioxidant‐phenolic compounds were not affected by irrigation with treated effluent compared with potable water. Our results demonstrate that both oregano and rosemary are suitable as industrial crops for essential oil and antioxidant production under irrigation with secondary‐treated municipal effluent because their yield quantity and quality were not affected.
A Model to Predict Safe Stages of Development for Rice Field Draining and Field Tests of the Model Predictions in the Arkansas Grand Prairie
Authors: Counce P. A. , Watkins K. B. , Brye K. R. , Siebenmorgen T. J.
Published: January 2009

Due to the cost of extracting water, effective and efficient utilization of irrigation water for rice (Oryza sativa L.) is critical to rice farm profitability. The objective of this study is to predict safe stages of development for draining rice. This objective has the potential of saving rice farmers water. A computer program has been developed to predict the stage of development for draining water from rice field soils at which the risk of reduced grain yield or milling quality from insufficient water is considered to be near zero. The parameters of the model are predictions of (i) temperature during rice reproductive growth stages (RRGS) starting at R3, (ii) timing of various RRGS, (iii) maximum amount of water used by the rice crop at each growth stage, and (iv) the water held in the soil profile after draining which is available to the rice crop. The central goals of the model are to allow draining at an RRGS in which (a) the danger of reducing yield and quality from water deficits is at a minimum and (b) water is conserved and land conditions for harvest are improved. Experiments to test the predictions were conducted in 2005 and 2006 at two Arkansas locations: Gillett and Stuttgart. An experiment was also conducted at DeWitt, AR, in 2006. Draining at stages of development predicted by the model did not affect yield milling quality relative to the control for any year or location. Predicted water savings from reduced irrigation ranged between $10.26 to $55.44 ha−1 depending on pump depth. Implementation of the program can save money, reduce tillage costs, and reduce unnecessary depletion of the aquifers.
Impact of Planting Date and Hybrid on Early Growth of Sweet Corn
Authors: y Garcia Axel Garcia , Guerra Larry C. , Hoogenboom Gerrit
Published: January 2009

Sweet corn (Zea mays L. var. rugosa) is a warm‐weather crop that is grown in most of the United States. Normally, it is planted over an extended planting window to provide a continuous supply for the fresh market. However, this planting window exposes the crop to various stresses and weather risks. The objective of this study was to determine the effect of planting date on early growth of sweet corn with different maturities for different environmental conditions in Georgia, USA. Three yellow sweet corn genotypes, including a full homozygous sugar enhanced (se), a super sweet (sh2), and a standard or normal (su), were compared in 2004, 2005, and 2006 in two locations in Georgia. The experiment consisted of one planting date in 2004, six in 2005, and four planting dates under two water regimes in 2006. Plant growth variables that were measured included leaf area index (LAI), canopy height, and aboveground biomass from emergence to the beginning of tasseling. The growth rate as a function of thermal time (TT) was used to determine the impact of planting date on growth of sweet corn. A base temperature (Tb) of 6.6°C for the three genotypes, obtained from experimental data, was used. Days to emergence varied from 4 to 12 for the warmest and coolest growing seasons, respectively. The growth of the three sweet corn genotypes showed a clear response to planting dates as LAI, canopy height, and aboveground biomass and the individual plant components, including stem, sheath, and leaves were significantly (P < 0.05) different at the beginning of tasseling. For all experiments, the longer the maturity group, the higher the total aboveground biomass. Significant differences (P < 0.05) for growth rate were found between planting dates, genotypes, plant components and their interactions. The short‐season hybrid tended to have a faster overall plant growth rate of all individual plant components during the warmer seasons. In contrast, the mid‐ and full‐season hybrids tended to have a higher growth rate during the cooler seasons. For rainfed conditions, the short‐season hybrid had higher leaf and sheath growth rates than the mid‐ and full‐season hybrids, resulting in a higher stem growth rate. These results indicate that the effect of planting date on early growth of sweet corn is of significance, as it may lead to identification of an optimum planting window for this crop.
Improving the Fermentation Characteristics of Corn through Agronomic and Processing Practices
Authors: Reicks Graig , Woodard Howard J. , Bly Anthony
Published: January 2009

This study determined the influence of corn (Zea mays L.) hybrids, N availability, grain harvest moisture, and drying temperatures on dry‐mill ethanol production. Six hybrids, ranging from 92 to 108 d in relative maturity (RM), were planted at two locations over 2 yr. One of four N fertilizer treatments were applied. Grain was hand‐harvested at grain moistures of 20 and 25%. Grain was dried to about 15% moisture at either 25, 38, 52, or 60°C in 2003, and 38, 66, 75, or 93°C in 2004. Ethanol was measured after grain was subjected to a small‐scale bench fermentation process. Grain yield increased at all four site‐years as available N increased to the recommended N application rate. Relative ethanol concentration was generally not affected by normal N fertilizer rates. Significant reductions in relative ethanol concentration occurred at the both the highest and lowest N rates in one‐of‐four site years. Hybrids designated as high fermentable starch (HS) by the company did not necessarily yield more ethanol than other hybrids. Ethanol concentration was reduced by 0.3% at Brookings for grain that was subjected to a killing frost. Ethanol concentration generally did not differ between grain dried at 38 and 52°C in 2003. Ethanol from grain harvested at 25% moisture and dried at 25°C was 0.1 to 0.3% lower than when grain was dried at 38 or 52°C. Drying temperatures of 25 to 52°C had no influence on relative ethanol concentration when the grain was harvested at 20% moisture. However, ethanol concentration was lowered 0.1 to 0.4% when drying temperature increased to 93°C in 2004. These results suggest that producers should apply the recommended N rates for maximum economic yield, plant adapted hybrids, and dry corn grain between 38 and 52°C to maximize relative ethanol concentration.
Zonejection: Conservation Tillage Manure Nutrient Delivery System
Authors: Coelho B. R. Ball , Roy R. C. , Bruin A. J. , More A. , White P.
Published: January 2009

Manure application in minimum till (MT) systems is a challenge worthy of attention because residue cover is a keystone for environmental protection. To develop a system combining zone tillage and manure application into one operation (zonejection), two experiments were conducted. In Exp. 1, liquid swine manure (LSM) was applied in fall or spring for two site years (A, B). In Exp. 2, LSM was zone‐applied either all preplant (PP) or split between preplant and sidedress (SP) for three site years (C, D, E). In both experiments, dietrich (DMI), vibro shank (VS), or subsurface deposition (SSD) applied the LSM, corn (Zea mays L.) was seeded in the manured zone, and NO3–N movement was monitored. Nutrients were supplied by inorganic fertilizer (IF) in control treatments under conventional till (CT), no till (NT), and zone till (ZT). With fall‐applied LSM, after a mild winter, more N was lost from the soil–plant system (i.e., 35 kg ha−1 soil NO3–N) than after a cold winter with snow cover (18 kg ha−1), and corn grain yield was reduced (by 1.2 Mg ha−1), even though supplemental fertilizer N was sidedressed. In Exp. 2, with LSM zoned all PP or SP, grain yield and N use efficiency were comparable to that with IF, except when double the crop N requirement was zoned all PP (Site D). Planting into a zone of concentrated LSM (3.4 S m−1) reduced grain yield when the LSM was injected by VS. With careful management, zonejection allows efficient utilization of manure nutrients while preserving residue cover.
Optimization of Crop Canopy Sensor Placement for Measuring Nitrogen Status in Corn
Authors: Roberts Darrin F. , Adamchuk Viacheslav I. , Shanahan John F. , Ferguson Richard B. , Schepers James S.
Published: January 2009

Active canopy sensors can be used to assess corn (Zea mays L.) N status and direct spatially‐variable in‐season N application. The goal of this study was to determine optimal sensor spacing for controlling whole‐ and/or split‐boom N application scenarios for a hypothetical 24‐row applicator. Sensor readings were collected from 24 consecutive rows at eight cornfields during vegetative growth in 2007 and 2008, and readings were converted to chlorophyll index (CI) values. A base map of measured CI values was created using square pixels equal to row spacing for each site (0.91 or 0.76 m in size). Sensor placement and boom section scenarios were evaluated using MSE (mean squared error) of calculated CI maps vs. the base CI map. Scenarios ranged from one sensor, one variable‐rate to 24 sensors, 24 variable‐rates for the hypothetical 24‐row applicator. The greatest reduction in MSE from the one variable‐rate scenario was obtained with 2 to 3 sensors estimating average CI for the entire boom width, unless each row was individually sensed. In every field, more accurate prediction of CI was obtained by averaging sensor readings across the entire 24 rows rather than predicting CI for more than two consecutive rows using only one sensor in each section. Because of the nature of spatial variability in CI, some fields may benefit from an increased number of sensors and/or boom sections equipped with 2 to 3 sensors each.
Planting Date and Cultivar Effects on Grain Yield in Dryland Corn Production
Authors: Kamara Alpha Y. , Ekeleme Friday , Chikoye David , Omoigui Lucky O.
Published: January 2009

Corn (Zea mays L.) production is gradually spreading into the Sudan savanna zone of West Africa where production is limited by erratic and inadequate rainfall. To increase corn production, production practices should be properly designed to minimize the effects of low precipitation and high temperatures that characterize the zone. A study, to determine the performance of late (120 d), early (90 d), and extra‐early maturing (80 d) corn cultivars over a range of planting dates, was performed in the Sudan savannas of northeast Nigeria. Delaying planting generally increased days to flowering and the anthesis‐silking interval (ASI) and reduced dry matter production and yield and yield components. In Azir, planting of corn on 13 July reduced grain yield by 42% in 2006 because of a dry spell during crop establishment. Delaying planting to 21 and 28 July also reduced grain yield by 19 and 28.5%, respectively over the 2 yr. Averaged over the 2‐yr yield reduction was 29.5 and 42% when corn was planted on 21 and 28 July, respectively in Damboa. There was no interaction between planting date and corn cultivar for days to silking, ASI, and grain yield suggesting that the cultivars responded similarly to planting date. The extra‐early maturing cultivar, 95 TZEE‐W, produced highest dry matter, harvest index, and grain yield at all planting dates suggesting that this cultivar is the most suitable in both locations. To reduce risk of drought stress, extra‐early maturing corn cultivars should be planted in the Sudan savanna between the last week of June and the first week of July.
Cattle Gain and Crop Yield for a Dryland Wheat‐Sorghum‐Fallow Rotation
Authors: Baumhardt R. L. , Schwartz R. C. , Greene L. W. , MacDonald J. C.
Published: January 2009

Increasing pumping costs and declining well capacities in the U.S. Southern High Plains have led to greater reliance on less productive and inherently riskier dryland cropping systems. Dryland wheat (Triticum aestivum L.) and grain sorghum [Sorghum bicolor (L.) Moench] are typically grown in a 3‐yr wheat‐sorghum‐fallow (WSF) rotation that may be intensified by integrating cattle (Bos taurus) grazing. Suitability of grazing dryland crops in the WSF rotation has not been evaluated. Our objectives were to quantify (i) cattle gain during limited grazing of dryland wheat and sorghum stover, and (ii) grazing effects on the growth and yield of the grazed wheat and subsequent sorghum crop. We established, concurrently, all WSF rotation phases in duplicate ungrazed and grazed plots in three replicated paddocks on a gently sloping Pullman silty clay loam (fine, mixed, superactive, thermic Torrertic Paleustoll) at the USDA‐ARS, Conservation and Production Research Laboratory, Bushland, TX (35°11′ N, 102°5′ W). Cattle gain, fallow soil water storage, and the growth and yield of wheat and subsequent grain sorghum were compared from 2000 to 2007 within a randomized complete block. Dryland wheat was grazed an average of 31 d during 7 of 8 test years by cattle stocked at 1.7 Mg ha−1 and produced a mean gain of 123 kg ha−1. Wheat grain yield averaged 1.72 Mg ha−1 without grazing and was not different from the 1.57 Mg ha−1 grain yield with grazing. Grazing decreased wheat straw yield, but subsequent soil water storage was unaffected. Sorghum grain yields of 2.26 Mg ha−1 in ungrazed plots were not different from grazed plots averaging 2.20 Mg ha−1. Overall productivity of the WSF cropping system was increased using limited grazing of dryland wheat forage and sorghum stover with no significant reduction in wheat or sorghum grain yields.
Regional Evaluation of Critical Nitrogen Concentrations in Winter Wheat Production of the North China Plain
Authors: Cui Zhenling , Zhang Fusuo , Dou Zhengxia , Yuxin Miao , Sun Qinping , Chen Xinping , Li Junliang , Ye Youliang , Yang Zhiping , Zhang Qiang , Liu Chunsheng , Huang Shaomin
Published: January 2009

Investigating critical nitrogen concentration (CNC) in grain and straw provides insights into N nutrition, and can serve as a guide to improved agricultural practice. This regional study evaluated the relationship between N fertilization rate and grain yield, N concentration, potential N loss, and determined critical grain and straw nitrogen concentrations (CGNC and CSNC) for winter wheat (Triticum aestivum L.) production in China. At the economically optimum nitrogen rate (EONR), grain N concentration was similar to the maximum value calculated using a linear plus plateau model, while straw N concentration was significantly less than the relevant maximum value. Soil nitrate N content after harvest and apparent N loss for maximum straw N concentration increased by 19 and 9 kg N ha−1 compared to values at the EONR. Based on nine field experiments, CGNC and CSNC corresponding to optimal N rate were established to be 21.9 g kg−1 (20.8–23.0 g kg−1) and 6.8 g kg−1 (6.5–7.1 g kg−1), respectively. An evaluation of CGNC and CSNC across 111 on‐farm sites indicated that while many sites had grain and straw N concentrations falling within the CGNC and CSNC, a substantial portion of the sites had grain and straw N concentrations falling outside of the CGNC and CSNC or falling within the critical ranges when N supply was deficient (0 N control) or excess (at farmer's N practice). This region‐wide study provided evidence for the usefulness of CSNC, and particularly CGNC, as indicators of N deficiencies in wheat production; however, neither indicator provided information about excess N fertilization.
Main‐Stem Node Removal Effect on Soybean Seed Yield and Composition
Authors: Conley Shawn P. , Pedersen Palle , Christmas Ellsworth P.
Published: January 2009

Hail injury to soybean [Glycine max L. (Merr.)] is common across the United States. Currently, U.S. hail adjusters use procedures that assume that yield reductions caused by stem cutoff and defoliation or defoliation without stem loss is similar during the vegetative development period. Our hypothesis was that seed yield will be affected by timing of node removal in vegetative soybean and that main‐stem node removal will influence seed composition. Research was conducted in Indiana and Iowa from 2003 to 2005 to test if removing 0, 20, 40, 60, 80, or 100% of nodes at V2, V6, or R3 development stages affects seed yield and grain composition. In Indiana, imposing node removal at the V2 stage resulted in 15.9% greater yield than imposing at the V6 stage. In Iowa, imposing node removal at the V2 stage on the average resulted in 24.9 and 46.1% greater seed yield than imposing node removal at the V6 or R3 stages, respectfully. Seed mass was 7.7% greater when comparing the V2 to the V6 node removal timing in Indiana. In Iowa, seed mass decreased 7.0% when 60% of the nodes were removed at V6 and 5.6% when 20% of the nodes were removed at R3. Soybean oil content was only affected by extreme node removal treatments while protein content was unaffected. Our results indicate that the soybean development stage that node removal occurs must be considered when estimating soybean seed yield loss and that an oil content adjustment is not needed to properly compensate growers for economic losses caused by node removal.
The Complexity of Enriched Mu-Calculi
Authors: Bonatti Piero A. , Lutz Carsten , Murano Aniello , Vardi Moshe Y.
Published: January 2009

The fully enriched μ-calculus is the extension of the propositional
μ-calculus with inverse programs, graded modalities, and nominals. While
satisfiability in several expressive fragments of the fully enriched
μ-calculus is known to be decidable and ExpTime-complete, it has recently
been proved that the full calculus is undecidable. In this paper, we study the
fragments of the fully enriched μ-calculus that are obtained by dropping at
least one of the additional constructs. We show that, in all fragments obtained
in this way, satisfiability is decidable and ExpTime-complete. Thus, we
identify a family of decidable logics that are maximal (and incomparable) in
expressive power. Our results are obtained by introducing two new automata
models, showing that their emptiness problems are ExpTime-complete, and then
reducing satisfiability in the relevant logics to these problems. The automata
models we introduce are two-way graded alternating parity automata over
infinite trees (2GAPTs) and fully enriched automata (FEAs) over infinite
forests. The former are a common generalization of two incomparable automata
models from the literature. The latter extend alternating automata in a similar
way as the fully enriched μ-calculus extends the standard μ-calculus.
Model Checking Probabilistic Timed Automata with One or Two Clocks
Authors: Jurdzinski Marcin , Laroussinie Francois , Sproston Jeremy
Published: January 2009

Probabilistic timed automata are an extension of timed automata with discrete
probability distributions. We consider model-checking algorithms for the
subclasses of probabilistic timed automata which have one or two clocks.
Firstly, we show that PCTL probabilistic model-checking problems (such as
determining whether a set of target states can be reached with probability at
least 0.99 regardless of how nondeterminism is resolved) are PTIME-complete for
one-clock probabilistic timed automata, and are EXPTIME-complete for
probabilistic timed automata with two clocks. Secondly, we show that, for
one-clock probabilistic timed automata, the model-checking problem for the
probabilistic timed temporal logic PCTL is EXPTIME-complete. However, the
model-checking problem for the subclass of PCTL which does not permit both
punctual timing bounds, which require the occurrence of an event at an exact
time point, and comparisons with probability bounds other than 0 or 1, is
PTIME-complete for one-clock probabilistic timed automata.
On the strength of proof-irrelevant type theories
Authors: Werner Benjamin
Published: January 2009

We present a type theory with some proof-irrelevance built into the
conversion rule. We argue that this feature is useful when type theory is used
as the logical formalism underlying a theorem prover. We also show a close
relation with the subset types of the theory of PVS. We show that in these
theories, because of the additional extentionality, the axiom of choice implies
the decidability of equality, that is, almost classical logic. Finally we
describe a simple set-theoretic semantics.
Canonical calculi with (n,k)-ary quantifiers
Authors: Avron Arnon , Zamansky Anna
Published: January 2009

Propositional canonical Gentzen-type systems, introduced in 2001 by Avron and
Lev, are systems which in addition to the standard axioms and structural rules
have only logical rules in which exactly one occurrence of a connective is
introduced and no other connective is mentioned. A constructive coherence
criterion for the non-triviality of such systems was defined and it was shown
that a system of this kind admits cut-elimination iff it is coherent. The
semantics of such systems is provided using two-valued non-deterministic
matrices (2Nmatrices). In 2005 Zamansky and Avron extended these results to
systems with unary quantifiers of a very restricted form. In this paper we
substantially extend the characterization of canonical systems to (n,k)-ary
quantifiers, which bind k distinct variables and connect n formulas, and show
that the coherence criterion remains constructive for such systems. Then we
focus on the case of k∈{0,1} and for a canonical calculus G show that it
is coherent precisely when it has a strongly characteristic 2Nmatrix, which in
turn is equivalent to admitting strong cut-elimination.
Game Refinement Relations and Metrics
Authors: de Alfaro Luca , Majumdar Rupak , Raman Vishwanath , Stoelinga Mariëlle
Published: January 2009

We consider two-player games played over finite state spaces for an infinite
number of rounds. At each state, the players simultaneously choose moves; the
moves determine a successor state. It is often advantageous for players to
choose probability distributions over moves, rather than single moves. Given a
goal, for example, reach a target state, the question of winning is thus a
probabilistic one: what is the maximal probability of winning from a given
state?
On these game structures, two fundamental notions are those of equivalences
and metrics. Given a set of winning conditions, two states are equivalent if
the players can win the same games with the same probability from both states.
Metrics provide a bound on the difference in the probabilities of winning
across states, capturing a quantitative notion of state similarity.
We introduce equivalences and metrics for two-player game structures, and we
show that they characterize the difference in probability of winning games
whose goals are expressed in the quantitative mu-calculus. The quantitative
mu-calculus can express a large set of goals, including reachability, safety,
and omega-regular properties. Thus, we claim that our relations and metrics
provide the canonical extensions to games, of the classical notion of
bisimulation for transition systems. We develop our results both for
equivalences and metrics, which generalize bisimulation, and for asymmetrical
versions, which generalize simulation.
Consistency and Completeness of Rewriting in the Calculus of Constructions
Authors: Walukiewicz-Chrzaszcz Daria , Chrzaszcz Jacek
Published: January 2009

Adding rewriting to a proof assistant based on the Curry-Howard isomorphism,
such as Coq, may greatly improve usability of the tool. Unfortunately adding an
arbitrary set of rewrite rules may render the underlying formal system
undecidable and inconsistent. While ways to ensure termination and confluence,
and hence decidability of type-checking, have already been studied to some
extent, logical consistency has got little attention so far. In this paper we
show that consistency is a consequence of canonicity, which in turn follows
from the assumption that all functions defined by rewrite rules are complete.
We provide a sound and terminating, but necessarily incomplete algorithm to
verify this property. The algorithm accepts all definitions that follow
dependent pattern matching schemes presented by Coquand and studied by McBride
in his PhD thesis. It also accepts many definitions by rewriting, containing
rules which depart from standard pattern matching.
Rational streams coalgebraically
Authors: Rutten J. J. M. M.
Published: January 2009

We study rational streams (over a field) from a coalgebraic perspective.
Exploiting the finality of the set of streams, we present an elementary and
uniform proof of the equivalence of four notions of representability of
rational streams: by finite dimensional linear systems; by finite stream
circuits; by finite weighted stream automata; and by finite dimensional
subsystems of the set of streams.
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
Authors: Buss Samuel R. , Hoffmann Jan , Johannsen Jan
Published: January 2009

Resolution refinements called w-resolution trees with lemmas (WRTL) and with
input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both
WRTL and WRTI when there is no regularity condition. For regular proofs, an
exponential separation between regular dag-like resolution and both regular
WRTL and regular WRTI is given.
It is proved that DLL proof search algorithms that use clause learning based
on unit propagation can be polynomially simulated by regular WRTI. More
generally, non-greedy DLL algorithms with learning by unit propagation are
equivalent to regular WRTI. A general form of clause learning, called
DLL-Learn, is defined that is equivalent to regular WRTL.
A variable extension method is used to give simulations of resolution by
regular WRTI, using a simplified form of proof trace extensions. DLL-Learn and
non-greedy DLL algorithms with learning by unit propagation can use variable
extensions to simulate general resolution without doing restarts.
Finally, an exponential lower bound for WRTL where the lemmas are restricted
to short clauses is shown.
On the Expressive Power of 2-Stack Visibly Pushdown Automata
Authors: Bollig Benedikt
Published: January 2009

Visibly pushdown automata are input-driven pushdown automata that recognize
some non-regular context-free languages while preserving the nice closure and
decidability properties of finite automata. Visibly pushdown automata with
multiple stacks have been considered recently by La Torre, Madhusudan, and
Parlato, who exploit the concept of visibility further to obtain a rich
automata class that can even express properties beyond the class of
context-free languages. At the same time, their automata are closed under
boolean operations, have a decidable emptiness and inclusion problem, and enjoy
a logical characterization in terms of a monadic second-order logic over words
with an additional nesting structure. These results require a restricted
version of visibly pushdown automata with multiple stacks whose behavior can be
split up into a fixed number of phases. In this paper, we consider 2-stack
visibly pushdown automata (i.e., visibly pushdown automata with two stacks) in
their unrestricted form. We show that they are expressively equivalent to the
existential fragment of monadic second-order logic. Furthermore, it turns out
that monadic second-order quantifier alternation forms an infinite hierarchy
wrt words with multiple nestings. Combining these results, we conclude that
2-stack visibly pushdown automata are not closed under complementation.
Finally, we discuss the expressive power of B\"{u}chi 2-stack visibly pushdown
automata running on infinite (nested) words. Extending the logic by an infinity
quantifier, we can likewise establish equivalence to existential monadic
second-order logic.
Bootstrapping Inductive and Coinductive Types in HasCASL
Authors: Schröder Lutz
Published: January 2009

We discuss the treatment of initial datatypes and final process types in the
wide-spectrum language HasCASL. In particular, we present specifications that
illustrate how datatypes and process types arise as bootstrapped concepts using
HasCASL's type class mechanism, and we describe constructions of types of
finite and infinite trees that establish the conservativity of datatype and
process type declarations adhering to certain reasonable formats. The latter
amounts to modifying known constructions from HOL to avoid unique choice; in
categorical terminology, this means that we establish that quasitoposes with an
internal natural numbers object support initial algebras and final coalgebras
for a range of polynomial functors, thereby partially generalising
corresponding results from topos theory. Moreover, we present similar
constructions in categories of internal complete partial orders in
quasitoposes.
A Brief Introduction to Algebraic Set Theory
Authors: Awodey Steve
Published: January 2009

This brief article is intended to introduce the reader to the field of algebraic set theory, in which models of set theory of a new and fascinating kind are determined algebraically. The method is quite robust, applying to various classical, intuitionistic, and constructive set theories. Under this scheme some familiar set theoretic properties are related to algebraic ones, while others result from logical constraints. Conventional elementary set theories are complete with respect to algebraic models, which arise in a variety of ways, such as topologically, type-theoretically, and through variation. Many previous results from topos theory involving realizability, permutation, and sheaf models of set theory are subsumed, and the prospects for further such unification seem bright.
A Natural Axiomatization of Computability and Proof of Church's Thesis
Authors: Dershowitz Nachum , Gurevich Yuri
Published: January 2009

Church's Thesis asserts that the only numeric functions that can be calculated by effective means are the recursive ones, which are the same, extensionally, as the Turing-computable numeric functions. The Abstract State Machine Theorem states that every classical algorithm is behaviorally equivalent to an abstract state machine. This theorem presupposes three natural postulates about algorithmic computation. Here, we show that augmenting those postulates with an additional requirement regarding basic operations gives a natural axiomatization of computability and a proof of Church's Thesis, as Gödel and others suggested may be possible. In a similar way, but with a different set of basic operations, one can prove Turing's Thesis, characterizing the effective string functions, and—in particular—the effectively-computable functions on string representations of numbers.
Cohen and Set Theory
Authors: Kanamori Akihiro
Published: January 2009

We discuss the work of Paul Cohen in set theory and its influence, especially the background, discovery, development of forcing.
Reconsidering Ordered Pairs
Authors: Scott Dana , McCarty Dominic
Published: January 2009

The well known Wiener-Kuratowski explicit definition of the ordered pair, which sets (x,y) = {{x}, {x,y}}, works well in many set theories but fails for those with classes which cannot be members of singletons. With the aid of the Axiom of Foundation, we propose arecursivedefinition of ordered pair which addresses this shortcoming and also naturally generalizes to ordered tuples of greater length. There are many advantages to the new definition, for it allows for uniform definitions working equally well in a wide range of models for set theories. In ZFC and closely related theories, the rank of an ordered pair of twoinfinite setsunder the new definition turns out to be equal to the maximum of the ranks of the sets.
Hyperlinear and Sofic Groups: A Brief Guide
Authors: Pestov Vladimir G.
Published: January 2009

This is an introductory survey of the emerging theory of two new classes of (discrete, countable) groups, called hyperlinear and sofic groups. They can be characterized as subgroups of metric ultraproducts of families of, respectively, unitary groups U(n) and symmetric groups Sn, n ∈ ℕ. Hyperlinear groups come from theory of operator algebras (Connes' Embedding Problem), while sofic groups, introduced by Gromov, are motivated by a problem of symbolic dynamics (Gottschalk's Surjunctivity Conjecture). Open questions are numerous, in particular it is still unknown if every group is hyperlinear and/or sofic.
Full Development of Tarski's Geometry of Solids
Authors: Gruszczyński Rafaŀ , Pietruszczak Andrzej
Published: January 2009

In this paper we give probably an exhaustive analysis of the geometry of solids which was sketched by Tarski in his short paper [20, 21]. We show that in order to prove theorems stated in [20, 21] one must enrich Tarski's theory with a new postulate asserting that the universe of discourse of the geometry of solids coincides with arbitrary mereological sums of balls, i.e., with solids. We show that once having adopted such a solution Tarski's Postulate 4 can be omitted, together with its versions 4′ and 4″. We also prove that the equivalence of postulates 4, 4′ and 4″ is not provable in any theory whose domain contains objects other than solids. Moreover, we show that the concentricity relation as defined by Tarski must be transitive in the largest class of structures satisfying Tarski's axioms.

We build a model (in three-dimensional Euclidean space) of the theory of so called T*-structures and present the proof of the fact that this is the only (up to isomorphism) model of this theory.

Moreover, we propose different categorical axiomatizations of the geometry of solids. In the final part of the paper we answer the question concerning the logical status (within the theory of T*-structures) of the definition of the concentricity relation given by Tarski.
A Survey of Propositional Realizability Logic
Authors: Plisko Valery
Published: January 2009

The study of propositional realizability logic was initiated in the 50th of the last century. Some interesting results were obtained in the 60-70th, but many important problems in this area are still open. Now interest to these problems from new generation of researchers is observed. This survey contains an exposition of the results on propositional realizability logic and corresponding techniques. Thus reading this paper can be the start point in exploring and development of constructive logic.
Bernays and Set Theory
Authors: Kanamori Akihiro
Published: January 2009

We discuss the work of Paul Bernays in set theory, mainly his axiomatization and his use of classes but also his higher-order reflection principles.
Actions of Groups of Finite Morley Rank on Small Abelian Groups
Authors: Deloro Adrien
Published: January 2009

We classify actions of groups of finite Morley rank on abelian groups of Morley rank 2: there are essentially two, namely the natural actions ofSL(V)andGL(V)withVa vector space of dimension 2. We also prove an identification theorem for the natural module of SL2in the finite Morley rank category.
Creatures on ω1 and weak diamonds
Authors: Mildenberger Heike
Published: January 2009

We specialise Aronszajn trees by an ωω-bounding forcing that adds reals. We work with creature forcings on uncountable spaces.

As an application of these notions of forcing, we answer a question of Moore, Hrušák and Džamonja whether implies the existence of a Souslin tree in a negative way by showing that “ and every Aronszajn tree is special” is consistent relative to ZFC.
Normal subgroups of infinite symmetric groups, with an application to stratified set theory
Authors: Bowler Nathan , Forster Thomas
Published: January 2009

It is generally known that infinite symmetric groups have few nontrivial normal subgroups (typically only the subgroups of bounded support) and none of small index. (We will explain later exactly what we mean by small). However the standard analysis relies heavily on the axiom of choice. By dint of a lot of combinatorics we have been able to dispense—largely—with the axiom of choice. Largely, but not entirely: our result is that if X is an infinite set with ∣X∣ = ∣X × X∣ then Symm(X) has no nontrivial normal subgroups of small index. Some condition like this is needed because of the work of Sam Tarzi who showed [4] that, for any finite group G, there is a model of ZF without AC in which there is a set X with Symm(X)/FSymm(X) isomorphic to G.

The proof proceeds in two stages. We consider a particularly useful class of permutations, which we call the class of flexible permutations. A permutation of X is flexible if it fixes at least ∣X∣-many points. First we show that every normal subgroup of Symm(X) (of small index) must contain every flexible permutation. This will be theorem 4. Then we show (theorem 7) that the flexible permutations generate Symm(X).
Borel-amenable reducibilities for sets of reals
Authors: Ros Luca Motto
Published: January 2009

We show that if ℱ is any “well-behaved” subset of the Borel functions and we assume the Axiom of Determinacy then the hierarchy of degrees on (ωω) induced by ℱ turns out to look like the Wadge hierarchy (which is the special case where ℱ is the set of continuous functions).
Topological dynamics of definable group actions
Authors: Newelski Ludomir
Published: January 2009

We interpret the basic notions of topological dynamics in the model-theoretic setting, relating them to generic types of definable group actions and their generalizations.
Decisive creatures and large continuum
Authors: Kellner Jakob , Shelah Saharon
Published: January 2009

For f, g ∈ ωω let be the minimal number of uniform g-splitting trees (or: Slaloms) to cover the uniform f-splitting tree, i.e., for every branch v of the f-tree, one of the g-trees contains v. is the dual notion: For every branch v, one of the g-trees guesses v(m) infinitely often.

It is consistent that for ℵ1 many pairwise different cardinals κ∊ and suitable pairs (f∊, g∊).

For the proof we use creatures with sufficient bigness and halving. We show that the lim-inf creature forcing satisfies fusion and pure decision. We introduce decisiveness and use it to construct a variant of the countable support iteration of such forcings, which still satisfies fusion and pure decision.
Zero-one law and definability of linear order
Authors: Niemistö Hannu
Published: January 2009

§1. Introduction. A logic ℒ has a limit law, if the asymptotic probability of every query definable in ℒ converges. It has a 0–1-law if the probability converges to 0 or 1. The 0–1-law for first-order logic on relational vocabularies was independently found by Glebski et al. [6] and Fagin [5]. Later it has been shown for many other logics, for instance for fragments of second order logic [12], for finite variable logic [13] and for FO extended with the rigidity quantifier [3]. Lynch [14] has shown a limit law for first-order logic on vocabularies with unary functions.

We say that two formulas or two logics are almost everywhere equivalent, if they are equivalent on a class of structures whose asymptotic probability measure is one [7]. A 0–1-law is usually proved by showing that every quantifier of the logic has almost everywhere quantifier elimination, i.e., every formula with just one quantifier in front of it is almost everywhere equivalent to a quantifier-free formula. Besides proving 0–1-law, this implies that the logic is (weakly) almost everywhere equivalent to first-order logic.

The aim of this paper is to study, whether a logic with a 0–1-law can have greater expressive power than FO in the almost everywhere sense and to what extent. In particular, we are interested on the definability of linear order. Because a 0–1-law determines the almost everywhere expressive power of the sentences of the logic completely, but does not say anything about formulas explicitly, we have to assume some regularity on logics. We will therefore mostly consider extensions of first-order logic with generalized quantifiers.
From index sets to randomness in ∅n: random reals and possibly infinite computations part II
Authors: Becher Verónica , Grigorieff Serge
Published: January 2009

We obtain a large class of significant examples ofn-random reals (i.e., Martin-Löf random in oracle ∅(n−1)) à la Chaitin. Any such real is defined as the probability that a universal monotone Turing machine performing possibly infinite computations on infinite (resp. finite large enough, resp. finite self-delimited) inputs produces an output in a given set. In particular, we develop methods to transfermany-one completeness results of index sets ton-randomness of associated probabilities.
On second order intuitionistic propositional logic without a universal quantifier
Authors: Zdanowski Konrad
Published: January 2009

We examine second order intuitionistic propositional logic, IPC2. Let ℱ∃ a be the set of formulas with no universal quantification. We prove Glivenko's theorem for formulas in ℱ∃ that is, for φ ∈ ℱ∃, φ is a classical tautology if and only if ┐┐φ is a tautology of IPC2. We show that for each sentence φ ∈ ℱ∃ (without free variables), φ is a classical tautology if and only if φ is an intuitionistic tautology. As a corollary we obtain a semantic argument that the quantifier ∀ is not definable in IPC2 from ⊥, ⋁, ⋀, →, ∃.
Towards a characterization of order-invariant queries over tame graphs
Authors: Benedikt Michael , Segoufin Luc
Published: January 2009

This work deals with the expressive power of logics on finite graphs with access to an additional “arbitrary” linear order. The queries that can be expressed this way are the order-invariant queries for the logic. For the standard logics used in computer science, such as first-order logic, it is known that access to an arbitrary linear order increases the expressiveness of the logic. However, when we look at the separating examples, we find that they have satisfying models whose Gaifman Graph is complex – unbounded in valence and in treewidth. We thus explore the expressiveness of order-invariant queries over well-behaved graphs. We prove that first-order order-invariant queries over strings and trees have no additional expressiveness over first-order logic in the original signature. We also prove new upper bounds on order-invariant queries over bounded treewidth and bounded valence graphs. Our results make use of a new technique of independent interest: the application of algebraic characterizations of definability to show collapse results.