We consider the problem of representing and reasoning about computer programs, and proposea translator from a core procedural iterative programming language to first-order logic with quantification over the domain of natural numbers that includes the usual successor function and the ``less than'' linear order, essentially a first-order logic with a discrete linear order. Unlike Hoare's logic, our approach does not rely on loop invariants. Unlike typical temporal logicspecification of a program, our translation does not require a transition system model of the program, and is compositional on the structures of the program. Some non-trivial examples are given to show the effectiveness of our translation for proving properties of programs.

Reiter's original proposal for default logic is unsatisfactory for open default theories because of Skolemization and grounding. In this paper, we reconsider this long-standing problem and propose a new world view semantics for first-order default logic. Roughly speaking, a world view of a first-order default theory is a maximal collection of structures satisfying the default theory where the default part is fixed by the world view itself. We show how this semantics generalizes classical first-order logic and first-order answer set programming, and we discuss its connections to Reiter's semantics and other related semantics. We also argue that first-order default logic under the world view semantics provides a rich framework for integrating classical logic based and rule based formalisms in the first-order case.

Artifact-centric systems are a recent paradigm for representing and implementing business processes. We present further results on the verification problem of artifact-centric systems specified by means of FO-CTL specifications. While the general problem is known to be undecidable, results in the literature prove decidability for artifact systems with infinite domains under boundedness and conditions such as uniformity. We here follow a different approach and investigate the general case with infinite domains. We show decidability of the model checking problem for the class of artifact-centric systems whose database schemas consist of a single unary relation, and we show that that the problem is undecidable if artifact systems are defined by using one binary relation or two unary relations.

Canonical (logic) programs (CP) refer to the class of normal programs (LP) augmented with connective not not , and  are equally expressive as propositional formulas (PF). In this paper we address the question of whether CP and PF are succinctly incomparable. Our main result shows that the PARITY problem only has exponential CP representations, while it can be polynomially represented in PF.  In other words, PARITY separates PF from CP. Simply speaking, this means that exponential size blowup is generally inevitable  when  translating a set of PF formulas into a (logically) equivalent CP program (without introducing new variables). Furthermore,  since it has been shown by Lifschitz and  Razborov  that there is also a problem which separates CP from PF (assuming P ⊈ NC 1 poly), it follows that the two formalisms are indeed succinctly incomparable.

Many knowledge representation tasks involve trees or similar structures as abstract datatypes.  However, devising compact and efficient declarative representations of such properties is non-obvious and can be challenging indeed.  In this paper, we take acyclicity properties into consideration and investigate logic-based approaches to encode them.  We use answer set programming as the primary representation language but also consider mappings to related formalisms, such as propositional logic, difference logic, and linear programming.

The situation calculus is a popular formalism for reasoning about actions and change. Since the language is first-order, reasoning in the situation calculus is undecidable in general.  An important question then is how to weaken reasoning in a principled way to guarantee decidability. Existing approaches either drastically limit the representation of the action theory or neglect important aspects such as sensing. In this paper we propose a model of limited belief for the epistemic situation calculus, which allows very expressive knowledge bases and handles both physical and sensing actions. The model builds on an existing approach to limited belief in the static case. We show that the resulting form of limited reasoning is sound with respect to the original epistemic situation calculus and eventually complete for a large class of formulas. Moreover, reasoning is decidable.

Logic programs with ordered disjunction (LPODs) (Brewka 2002) generalize normal logic programs by combining alternative and ranked options in the heads of rules. It has been showed that LPODs are useful in a number of areas including game theory, policy languages, planning and argumentations. In this paper, we extend propositional LPODs to the first-order case, where a classical second-order formula is defined to capture the stable model semantics of the underlying first-order LPODs. We then develop a progression semantics that is equivalent to the stable model semantics but naturally represents the reasoning procedure of LPODs. We show that on finite structures, every LPOD can be translated to a first order sentence, which provides a basis for computing stable models of LPODs. We further study the complexity and expressiveness of LPODs and prove that almost positive LPODs precisely capture first-order normal logic programs, which indicates that ordered disjunction itself and constraints are sufficient to represent negation as failure.

First-order model counting emerged recently as a novel reasoning task, at the core of efficient algorithms for probabilistic logics. We present a Skolemization algorithm for model counting problems that eliminates existential quantifiers from a first-order logic theory without changing its weighted model count. For certain subsets of first-order logic, lifted model counters were shown to run in time polynomial in the number of objects in the domain of discourse, where propositional model counters require exponential time. However, these guarantees apply only to Skolem normal form theories (i.e., no existential quantifiers) as the presence of existential quantifiers reduces lifted model counters to propositional ones. Since textbook Skolemization is not sound for model counting, these restrictions precluded efficient model counting for directed models, such as probabilistic logic programs, which rely on existential quantification. Our Skolemization procedure extends the applicability of first-order model counters to these representations. Moreover, it simplifies the design of lifted model counting algorithms.

We present a cognitive design assistance system equipped with analytical capabilities aimed at anticipating architectural building design performance with respect to people-centred functional design goals. The paper focuses on the system capability to generate "narratives of visuo-locomotive user experience" from digital computer-aided architecture design (CAAD) models. The system is based on an underlying declarative narrative representation and computation framework pertaining to conceptual, geometric, and qualitative spatial knowledge. The semantics of the declarative narrative model, i.e., the overall   representation and computation model, is founded on: (a). conceptual knowledge formalised in an OWL ontology; (b). a general spatial representation and reasoning engine implemented in constraint logic programming; and (c). a declaratively encoded (narrative) construction process (based on search over graph structures) implemented in answer-set programming. We emphasise and demonstrate: complete system implementation, scalability, and robust performance & integration with industry-scale architecture industry tools (e.g., Revit, ArchiCAD) & standards (BIM, IFC).

Golog and ConGolog are languages defined in the situation calculus for cognitive robotics. Given a Golog program \delta, its semantics is defined by a macro Do(\delta,s,s') that expands to a logical sentence that captures the conditions under which performing \delta in s can terminate in s'. A similarmacro is defined for ConGolog programs. In general, the logical sentences that these macros expand to are second-order, and in the case of ConGolog, may involve quantification over programs. In this paper, we show that by making use of the foundational axioms in the situation calculus, in particular, the second-order closure axiom about the space of situations, these macro expressions can actually be defined using first-order sentences.