Logic & Formal Reasoning
Fiascomatic: A Framework for Automated Fiasco Playsets
Horswill, Ian D. (Northwestern University)
We present Fiascomatic , a mixed initiative system for generating consistent scenarios for the indie storytelling RPG Fiasco . Players can repeatedly generate scenarios, locking down aspects of a scenario they like and regenerating aspects they donโt, until they arrive at a scenario they find entertaining.ย It is not a story generation system; it generates scenarios from which players then generate stories.ย Nor is it intended to generate optimal scenarios; it generates random scenarios which the players can then curate according to their taste. Fiascomatic presents an interesting intermediate point between non-automated table-top RPGs and fully automated systems such as story generators or autonomous characters.ย It is a tool that can be used by Fiasco players to speed the generation of game setups while preserving creative input on the part of the players, and by Fiasco playset authors to make automated playsets.
Planning in RTS Games with Incomplete Action Definitions via Answer Set Programming
Balduccini, Marcello (Drexel University) | Uriarte, Alberto (Drexel University) | Ontaรฑรณn, Santiago (Drexel University)
Standard game tree search algorithms, such as minimax or Monte Carlo Tree Search, assume the existence of an accurate forward model that simulates the effects of actions in the game. Creating such model, however, is a challenge in itself.One cause of the complexity of the task is the gap in level of abstraction between the informal specification of the model and its implementation language. To overcome this issue, we propose a technique for the implementation of forward models that relies on the Answer Set Programming paradigm and on well-established knowledge representation techniques from defeasible reasoning and reasoning about actions and change. We evaluate our approach in the context of Real-Time Strategy games using a collection of StarCraft scenarios.
Playspecs: Regular Expressions for Game Play Traces
Osborn, Joseph Carter (University of California, Santa Cruz) | Samuel, Ben (University of California, Santa Cruz) | Mateas, Michael (University of California, Santa Cruz) | Wardrip-Fruin, Noah (University of California, Santa Cruz)
We introduce Playspecs, an application of omega-regular expressions to specifying play traces (sequences of game states or events unfolding over time). This connects the automated analysis and model checking of games to the literature on formal software verification via Bu ฬchi automata. We show how to define desirable or undesirable sequences of game events with Playspecs and how associated algorithms can find examples (or prove the impossibility) of such sequences. Playspecs have two main benefits over existing techniques for specifying the behaviors of a game over time. First, they offer a scalable commitment to formal modeling: the same Playspecs can filter existing traces gathered by telemetry, search for satisfying traces using existing game code, or drive formal verification when paired with a logical model of a game. Second, Playspecs' syntax can be customized for the game engine or game in question so designers may write specifications using their game's native vocabulary. We define Playspecs' syntax and semantics (modulo gamespecific customizations) and outline algorithms for each of the applications mentioned above, providing examples from the social simulation game Prom Week and the puzzle game engine PuzzleScript.
Ceptre: A Language for Modeling Generative Interactive Systems
Martens, Chris (Carnegie Mellon University)
We present a rule specification language called Ceptre,intended to enable rapid prototyping for experimental game mechanics, especially in domains that depend on procedural generation and multi-agent simulation. Ceptre can be viewed as an explication of a new methodology for understanding games based on linear logic, a formal logic concerned with resource usage. We present a correspondence between gameplay and proof search in linear logic, building on prior work on generating narratives. In Ceptre, we introduce the ability to add interactivity selectively into a generative model, enabling inspection of intermediate states for debugging and exploration as well as a means of play. We claim that this methodology can support game designers and researchers in designing, anaylzing, and debugging the core systems of their work in generative, multi-agent gameplay. To support this claim, we provide two case studies implemented in Ceptre, one from interactive narrative and one from a strategy-like domain.
Towards a General Framework for Actual Causation Using CP-logic
Beckers, Sander, Vennekens, Joost
Since Pearl's seminal work on providing a formal language for causality, the subject has garnered a lot of interest among philosophers and researchers in artificial intelligence alike. One of the most debated topics in this context regards the notion of actual causation, which concerns itself with specific - as opposed to general - causal claims. The search for a proper formal definition of actual causation has evolved into a controversial debate, that is pervaded with ambiguities and confusion. The goal of our research is twofold. First, we wish to provide a clear way to compare competing definitions. Second, we also want to improve upon these definitions so they can be applied to a more diverse range of instances, including non-deterministic ones. To achieve these goals we will provide a general, abstract definition of actual causation, formulated in the context of the expressive language of CP-logic (Causal Probabilistic logic). We will then show that three recent definitions by Ned Hall (originally formulated for structural models) and a definition of our own (formulated for CP-logic directly) can be viewed and directly compared as instantiations of this abstract definition, which allows them to deal with a broader range of examples.
Improved Answer-Set Programming Encodings for Abstract Argumentation
Gaggl, Sarah A., Manthey, Norbert, Ronca, Alessandro, Wallner, Johannes P., Woltran, Stefan
The design of efficient solutions for abstract argumentation problems is a crucial step towards advanced argumentation systems. One of the most prominent approaches in the literature is to use Answer-Set Programming (ASP) for this endeavor. In this paper, we present new encodings for three prominent argumentation semantics using the concept of conditional literals in disjunctions as provided by the ASP-system clingo. Our new encodings are not only more succinct than previous versions, but also outperform them on standard benchmarks.
Disjunctive Answer Set Solvers via Templates
Brochenin, Remi, Lierler, Yuliya, Maratea, Marco
Answer set programming is a declarative programming paradigm oriented towards difficult combinatorial search problems. A fundamental task in answer set programming is to compute stable models, i.e., solutions of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has a stable model is $\Sigma^P_2$-complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely DLV, GnT, Cmodels, CLASP and WASP. In this paper we show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for disjunctive answer set solvers. Transition systems give a unifying perspective and bring clarity in the description and comparison of solvers. They can be effectively used for analyzing, comparing and proving correctness of search algorithms as well as inspiring new ideas in the design of disjunctive answer set solvers. In this light, we introduce a general template, which accounts for major techniques implemented in disjunctive solvers. We then illustrate how this general template captures solvers DLV, GnT and Cmodels. We also show how this framework provides a convenient tool for designing new solving algorithms by means of combinations of techniques employed in different solvers.
Query-Answer Causality in Databases: Abductive Diagnosis and View-Updates
Salimi, Babak, Bertossi, Leopoldo
Causality has been recently introduced in databases, to model, characterize and possibly compute causes for query results (answers). Connections between query causality and consistency-based diagnosis and database repairs (wrt. integrity constrain violations) have been established in the literature. In this work we establish connections between query causality and abductive diagnosis and the view-update problem. The unveiled relationships allow us to obtain new complexity results for query causality -the main focus of our work- and also for the two other areas.
Learning Regular Languages over Large Ordered Alphabets
Mens, Irini-Eleftheria, Maler, Oded
This work is concerned with regular languages defined over large alphabets, either infinite or just too large to be expressed enumeratively. We define a generic model where transitions are labeled by elements of a finite partition of the alphabet. We then extend Angluin's L* algorithm for learning regular languages from examples for such automata. We have implemented this algorithm and we demonstrate its behavior where the alphabet is a subset of the natural or real numbers. We sketch the extension of the algorithm to a class of languages over partially ordered alphabets.
Non-normal modalities in variants of Linear Logic
Porello, Daniele, Troquard, Nicolas
This article presents modal versions of resource-conscious logics. We concentrate on extensions of variants of Linear Logic with one minimal non-normal modality. In earlier work, where we investigated agency in multi-agent systems, we have shown that the results scale up to logics with multiple non-minimal modalities. Here, we start with the language of propositional intuitionistic Linear Logic without the additive disjunction, to which we add a modality. We provide an interpretation of this language on a class of Kripke resource models extended with a neighbourhood function: modal Kripke resource models. We propose a Hilbert-style axiomatization and a Gentzen-style sequent calculus. We show that the proof theories are sound and complete with respect to the class of modal Kripke resource models. We show that the sequent calculus admits cut elimination and that proof-search is in PSPACE. We then show how to extend the results when non-commutative connectives are added to the language. Finally, we put the logical framework to use by instantiating it as logics of agency. In particular, we propose a logic to reason about the resource-sensitive use of artefacts and illustrate it with a variety of examples.