Abstract The analytic technique for proving completeness gives a very operational perspective: build a countermodel to the unproved formula from a failed proof attempt in your calculus. We have to be careful, however, that the proof attempt did not fail because our strategy in finding it was flawed. Overcoming this concern requires designing a prover. We design and formalize in Isabelle/HOL a sequent calculus prover for first-order logic with functions. We formalize soundness and completeness theorems using an existing framework and extract executable code to Haskell. The crucial idea is to move complexity from the prover itself to a stream of instructions that it follows. The result serves as a minimal example of the analytic technique, a naive prover for first-order logic, and a case study in formal verification.

Abstract We formalize in Isabelle/HOL soundness and completeness of a one-sided sequent calculus for first-order logic. The completeness is shown via a translation from a semantic tableau calculus, whose completeness proof we base on the theory entry ‘First-Order Logic According to Fitting’ by Berghofer in the Archive of Formal Proofs. The calculi and proof techniques are taken from Ben-Ari’s textbook Mathematical Logic for Computer Science (Springer, 2012). We thereby demonstrate that Berghofer’s approach works not only for natural deduction but also constitutes a framework for mechanically checked completeness proofs for a range of proof systems.

Demonstrating reliability of cognitive multi-agent systems is of key importance. There has been an extensive amount of work on logics for verifying cognitive agents but it has remained mostly theoretical. Cognitive agent-oriented programming languages provide the tools for compact representation of complex decision making mechanisms, which offers an opportunity for applying a theorem proving approach. We base our work on the belief that theorem proving can add to the currently available approaches for providing assurance for cognitive multi-agent systems. However, a practical approach using theorem proving is missing. We explore the use of proof assistants to make verifying cognitive multi-agent systems more practical.

Understanding the social contexts in which actions and interactions take place is of utmost importance for planning one’s goals and activities. People use social practices as means to make sense of their environment, assessing how that context relates to past, common experiences, culture and capabilities. Social practices can therefore simplify deliberation and planning in complex contexts. In the context of patient-centered planning, hospitals seek means to ensure that patients and their families are at the center of decisions and planning of the healthcare processes. This requires on one hand that patients are aware of the practices being in place at the hospital and on the other hand that hospitals have the means to evaluate and adapt current practices to the needs of the patients. In this paper we apply a framework for formalizing social practices of an organization to an emergency department that carries out patient-centered planning. We indicate how such a formalization can be used to answer operational queries about the expected outcome of operational actions.

SyntaxTrain parses a Java program and displays the syntax diagrams associated with a syntax error.

The information state of an agent is changed when a text (in natural language) is processed. The meaning of a text can be taken to be this information state change potential. The inference of a consequence make explicit something already implicit in the premises --- i.e. that no information state change occurs if the (assumed) consequence text is processed after the (given) premise texts have been processed. Elementary logic (i.e. first-order logic) can be used as a logical representation language for texts, but the notion of a information state (a set of possibilities --- namely first-order models) is not available from the object language (belongs to the meta language). This means that texts with other texts as parts (e.g. propositional attitudes with embedded sentences) cannot be treated directly. Traditional intensional logics (i.e. modal logic) allow (via modal operators) access to the information states from the object language, but the access is limited and interference with (extensional) notions like (standard) identity, variables etc. is introduced. This does not mean that the ideas present in intensional logics will not work (possibly improved by adding a notion of partiality), but rather that often a formalisation in the simple type theory (with sorts for entities and indices making information states first class citizens --- like individuals) is more comprehensible, flexible and logically well-behaved.