Arbitrary public announcement logic ) reasons about how the knowledge of a set of agents changes after true public announcements and after arbitrary announcements of true epistemic formulas. We consider a variant of arbitrary public announcement logic called positive arbitrary public announcement logic ), which restricts arbitrary public announcements to announcement of positive formulas. Positive formulas prohibit statements about the ignorance of agents. The positive formulas correspond to the universal fragment in first-order logic. As two successive announcements of positive formulas (...) need not correspond to the announcement of a positive formula, \ is rather different from \. We show that \ is more expressive than public announcement logic \, and that \ is incomparable with \. We also provide a sound and complete infinitary axiomatisation. (shrink)

Tim French, Wiebe van der Hoek, Petar Iliev and Barteld Kooi. Succinctness of Epistemic Languages. In: T. Walsh (editor). Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-11), pp. 881-886, AAAI Press, Menlo Park.

This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic, group announcement logic, and coalition announcement logic. In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents all of which are simultaneously making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that group (...) may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics. (shrink)

This paper demonstrates the undecidability of a number of logics with quantification over public announcements: arbitrary public announcement logic, group announcement logic, and coalition announcement logic. In APAL we consider the informative consequences of any announcement, in GAL we consider the informative consequences of a group of agents all of which are simultaneously making known announcements. So this is more restrictive than APAL. Finally, CAL is as GAL except that we now quantify over anything the agents not in that group (...) may announce simultaneously as well. The logic CAL therefore has some features of game logic and of ATL. We show that when there are multiple agents in the language, the satisfiability problem is undecidable for APAL, GAL, and CAL. In the single agent case, the satisfiability problem is decidable for all three logics. (shrink)

We examine various logics that combine knowledge, awareness, and change of awareness. An agent can become aware of propositional propositions but also of other agents or of herself. The dual operation to becoming aware, forgetting, can also be modelled. Our proposals are based on a novel notion of structural similarity that we call awareness bisimulation, the obvious notion of modal similarity for structures encoding knowledge and awareness.

In mining, manufacturing and industrial process industries, maintenance procedures are used as an aid to guide technicians through complex manual tasks. These procedures are not machine-readable, and cannot support reasoning in digitally integrated manufacturing systems. Procedure documents contain unstructured text and are stored in a variety of formats. The aim of this work is to query information held in real industrial maintenance procedures. To achieve this, we develop an ontology for maintenance procedures using the OWL 2 description language. We leverage (...) classes and object properties from the ISO 15926 Part 14 Upper Ontology and create a domain ontology. The key contribution of this paper is a demonstration of trade-offs required when modelling an existing engineering artifact, where an abstraction of its contents is given a-priori. We provide an ontologically rigorous abstraction of notions captured in procedure documentation to a set of classes, relations and axioms that allow reasoning over the contents. Validation of the ontology is performed via a series of competency questions based on queries relevant to technicians, engineers and schedulers in industry. The ontology is applied to real world maintenance procedures from two industrial organisations. (shrink)

This volume examines some of the most contentious social justice issues present in the corpus of Augustine's writings. Whether one is concerned with human trafficking and the contemporary slave trade, the global economy, or endless wars, these essays further the conversation on social justice as informed by the writings of Augustine of Hippo.

We consider the relation between the uniform interpolation property and the elimination of non-standard quantifiers (the bisimulation quantifiers) in the context of the ?-calculus. In particular, we isolate classes of frames where the correspondence between these two properties is nicely smooth.

RésuméLe Dr French résume ici très briévement les idées développées dans un ouvrage qu'il publiera prochainement sous le titre Intégration of behavior . – Le comportement comprend deux aspects essentiels que ľon peut désigner des termes de motivation et compréhension intelligente {insight). Cette dernière àété admirablement analľsée par ľécole gestaltiste , qui à cependant eu le tort de la présenter comme de soi consciente. Or, il ľà des insights inconscients, áľœuvre par exemple dans ľacquisition des réflexes conditionnels, des habiletés motrices (...) et de certaines réactions pathologiques. Conscient ou inconscient, ľinsight implique un groupement sľstématique des données sensorielles, non plus considérées isolément, mais mises en relation les unes avec les autrès.La manifestation la plus simple ?insight est la construction ?un champ cognitif qui choisit et groupe les données élémentaires, et fait répondre, non plus à ces données séparément, mais à leur groupement. Le cognitive field peut demeurer purement cognitif. II prend le nom de champ intégratif lorsqu'il exerce une influence régulatrice sur le comportement. Ces champs intégratifs ne restent pas isolés. lis interfèrent et se combinent entre eux, par exemple dans ľaction à long terme, par un processus de résonance ou ?induction mutuelle. Ceci joue notamment dans les cas ou ľindividu fait des plans relativement à un but éloigné. Une induction mutuelle s'établit alors entre le champ de ľimagination et celui de la réalité et de la perception.Champs cognitifs et intégratifs sont activeés par des pressions motivationnelles ?intensité variable. II faut ici distinguer entre pressions purement négatives, qui poussent ľindividu àéchapper à un état de dissatisfaction et tendent à se décharger en activités musculaires diffuses, et pressions positives, stimulées par ľespoir et par la présence ou le souvenir ?une satisfaction possible dans ľenvironnement. Besoins et espoirs jouent dans le comportement un rôle complémentaire. Ľespoir substitue á la primitive décharge motrice caractéristique des besoins, une activité canalisée et orientée vers le but. Ceci, qui peut être inné dans les espèces animales inférieures, est chez ľhomme matière ?apprentissage. Pour atteindre un but, ľhomme doit apprendre á inhiber les décharges motrices originelles, et á leur substituer une conduite guidée par ľespoir, les mécanismes ?intégration et la construction de plans.Le succès de cette entreprise dépend de ľintensité de la pression motivationnelle. Si celle‐ci dépasse certaines limites , les mécanismes ?intégration et ?élaboration de plans sont rendus plus difficiles et Ľindividuperd la tête, c'est‐à‐dire que Ľinsight régulateur ne peut plus contrôler les décharges motrices. Comme c'est ľespoir du succès qui déclenche le travail ?intégration et de prévision, la capacityé?intégration ?un individu dans une circonstance donnée augmente en proportion de ses espoirs de succès et diminue en proportion de ses appréhensions ?échec.Ces considérations nous acheminent jusqu'aux réactions pathologiques, névrotiques et psychotiques, dont s'occupe la psychanalyse. Dans ces comportements irrationnels, les mécanismes ?intégration ont, sous ľeffet des facteurs qui viennent ?être indiqués, subi une sorte de fragmentation, suivie ?habitude par des réintégrations partielles de certains de leurs fragments. (shrink)

This paper compares the recently proposed Robust Full Computational Tree Logic to model robustness in concurrent systems with other computational tree logic -based logics. RoCTL* extends CTL* with the addition of the operators Obligatory and Robustly, which quantify over failure-free paths and paths with one more failure respectively. This paper focuses on examining the succinctness and expressiveness of RoCTL* by presenting translations to and from RoCTL*. The core result of this paper is to show that RoCTL* is expressively equivalent to (...) CTL* but is non-elementarily more succinct. That is, RoCTL* does not add any expressive power over CTL*, but can represent some properties using vastly reduced formulae. We present a translation from RoCTL* into CTL* that preserves truth but may result in non-elementary growth in the length of the translated formula, as each nested Robustly operator may result in an extra exponential blowup. However, we show that this translation is optimal in the sense th.. (shrink)