Conditional male dimorphism and alternative reproductive tactics in a Neotropical arachnid (Opiliones)

In arthropods, most cases of morphological dimorphism within males are the result of a conditional evolutionarily stable strategy (ESS) with status-dependent tactics. In conditionally male-dimorphic species, the status` distributions of male morphs often overlap, and the environmentally cued threshold model (ET) states that the degree of overlap depends on the genetic variation in the distribution of the switchpoints that determine which morph is expressed in each value of status. Here we describe male dimorphism and alternative mating behaviors in the harvestman Serracutisoma proximum. Majors express elongated second legs and use them in territorial fights; minors possess short second legs and do not fight, but rather sneak into majors` territories and copulate with egg-guarding females. The static allometry of second legs reveals that major phenotype expression depends on body size (status), and that the switchpoint underlying the dimorphism presents a large amount of genetic variation in the population, which probably results from weak selective pressure on this trait. With a mark-recapture study, we show that major phenotype expression does not result in survival costs, which is consistent with our hypothesis that there is weak selection on the switchpoint. Finally, we demonstrate that switchpoint is independent of status distribution. In conclusion, our data support the ET model prediction that the genetic correlation between status and switchpoint is low, allowing the status distribution to evolve or to fluctuate seasonally, without any effect on the position of the mean switchpoint.

Analytic Methods for the Logic of Proofs

The logic of proofs (lp) was proposed as Gdels missed link between Intuitionistic and S4-proofs, but so far the tableau-based methods proposed for lp have not explored this closeness with S4 and contain rules whose analycity is not immediately evident. We study possible formulations of analytic tableau proof methods for lp that preserve the subformula property. Two sound and complete tableau decision methods of increasing degree of analycity are proposed, KELP and preKELP. The latter is particularly inspired on S4-proofs. The crucial role of proof constants in the structure of lp-proofs methods is analysed. In particular, a method for the abduction of proof constant specifications in strongly analytic preKELP proofs is presented; abduction heuristics and the complexity of the method are discussed.

A logic-based agent that plans for extended reachability goals

Planning to reach a goal is an essential capability for rational agents. In general, a goal specifies a condition to be achieved at the end of the plan execution. In this article, we introduce nondeterministic planning for extended reachability goals (i.e., goals that also specify a condition to be preserved during the plan execution). We show that, when this kind of goal is considered, the temporal logic CTL turns out to be inadequate to formalize plan synthesis and plan validation algorithms. This is mainly due to the fact that the CTL`s semantics cannot discern among the various actions that produce state transitions. To overcome this limitation, we propose a new temporal logic called alpha-CTL. Then, based on this new logic, we implement a planner capable of synthesizing reliable plans for extended reachability goals, as a side effect of model checking.

New Improvements in Automatic Structure Elucidation Using the LSD (Logic for Structure Determination) and the SISTEMAT Expert Systems

This article describes the integration of the LSD (Logic for Structure Determination) and SISTEMAT expert systems that were both designed for the computer-assisted structure elucidation of small organic molecules. A first step has been achieved towards the linking of the SISTEMAT database with the LSD structure generator. The skeletal descriptions found by the SISTEMAT programs are now easily transferred to LSD as substructural constraints. Examples of the synergy between these expert systems are given for recently reported natural products.