Workshop Description

Human reasoning or the psychology of deduction is well researched in cognitive psychology and in cognitive science. There are a lot of findings which are based on experimental data about reasoning tasks, among others models for the selection task or the suppression task discussed by Byrne and others. This research is supported also by brain researchers, who aim at localizing reasoning processes within the brain. Automated deduction, on the other hand, is mainly focusing on the automated proof search in logical calculi. And indeed there is tremendous success during the last decades. Recently a coupling of the areas of cognitive science and automated reasoning is addressed in several approaches. For example there is increasing interest in modelling human reasoning within automated reasoning systems including modeling with answer set programming, deontic logic or abductive logic programming. There are also various approaches within AI research. This workshop is a follow-up event of the successful Bridging workshop ( which was located at CADE-25. Like its preceding event, it is intended to get an overview of existing approaches and make a step towards a cooperation between computational logic and cognitive science. Topics of interest include, but are not limited to the following:
  • Limits and differences between automated and human reasoning
  • Psychology of deduction
  • Common sense reasoning
  • Logics modeling human cognition
  • Modeling human reasoning using automated reasoning systems
  • Non-monotonic, defeasible, and classical reasoning and possible explanations for human reasoning
  • Application fields of automated reasoning in the interaction with human reasoners
  • The workshop will be held in conjunction with IJCAI-16 and is supported by IFIP TC12.

    Invited Speaker

    Sangeet Khemlani, Naval Research Laboratory in Washington DC.

    List of important dates

  • Full Paper submission deadline: April 18th, 2016
  • Notification: May 27th, 2016
  • Final submission: June 10th, 2016
  • Workshop: July 9th, 2016
  • Submission and Contribution Format

    Papers, including the description of work in progress are welcome and should be formatted according to the Springer LNCS guidelines. The length should not exceed 15 pages. All papers must be submitted in PDF. Formatting instructions and the LNCS style files can be obtained at The EasyChair submission site is available at


    Proceedings of the workshop will be published as CEUR workshop proceedings. Depending on the number and quality of the submission we are planning post proceedings in the Springer AICT Series A preliminary version of the proceedings can be found here.


  • Ulrich Furbach, University of Koblenz
  • Steffen Hoelldobler, University of Dresden
  • Marco Ragni, University of Freiburg
  • Natarajan Shankar, SRI International
  • Contact: Claudia Schon
  • Program Committee

  • Ruth Byrne, University of Dublin
  • Ulrich Furbach, University of Koblenz
  • Steffen Hoelldobler, University of Dresden
  • Antonis C. Kakas, University of Cyprus
  • Gabriele Kern-Isberner, TU Dortmund University
  • Kai-Uwe Kuehnberger, University of Osnabrueck
  • Laura Martignon, MPI Berlin
  • Ursula Martin, University of Oxford
  • Luis Moniz Pereira, Universidade Nova de Lisboa
  • Marco Ragni, University of Freiburg
  • Claudia Schon, University of Koblenz
  • Natarajan Shankar, SRI International
  • Keith Stenning, Edinburgh University
  • Frieder Stolzenburg, Harz University of Applied Sciences
  • Contact: Claudia Schon

    Accepted Papers

    Naveen Sundar Govindarajulu and Selmer Bringsjord. Crowdsourcing Theorem Proving via Natural Games
    Abstract: Despite the science of modern formal reasoning being more than a century old, mechanized formal reasoning is nowhere near what expert human reasoners (formal and informal) can achieve. Meanwhile, there is a steadily increasing need for automated theorem proving in various fields of science and engineering: proof discovery and verification in science and mathematics, formal verification for hardware and software and logic-based AI are all based on formal theorem proving. We present initial results from a project on helping automated theorem provers with crowdsourced theorem proving through games.
    Ana Costa, Emmanuelle-Anna Dietz, Steffen Hölldobler and Marco Ragni. Syllogistic Reasoning under the Weak Completion Semantics
    Abstract: In a recent meta-analysis, Khemlani & Johnson-Laird (2012) showed that the conclusions drawn by human reasoners in psychological experiments about syllogistic reasoning are not the conclusions predicted by classical first-order logic. Moreover, current cognitive theories deviate significantly from the empirical data. In this paper we show how human syllogistic reasoning can be modelled under weak completion semantics, a new cognitive theory.
    Aaron Sloman. Natural Vision and Mathematics: Seeing Impossibilities
    Abstract: The Turing-inspired Meta-Morphogenesis project investigates forms of biological information processing produced by evolution since the earliest life forms, especially information processing mechanisms that made possible the deep mathematical discoveries of Euclid, Archimedes, and other ancient mathematicians. Such mechanisms must enable perception of possibilities and constraints on possibilities - types of affordance perception not explicitly discussed by Gibson, but suggested by his ideas. Current AI vision and reasoning systems lack such abilities. A future AI project might produce a design for "baby" robots that can "grow up" to become mathematicians able to replicate (and extend) some of the ancient discoveries, e.g. in the way that Archimedes extended Euclidean geometry to make trisection of an arbitrary angle possible. This is relevant to many kinds of intelligent organism or machine perceiving and interacting with structures and processes in the environment. This would demonstrate the need to extend Dennett's taxonomy of types of mind to include Euclidean (or Archimedean) minds, and would support Immanuel Kant's philosophy of mathematics.
    Marco Ragni, Emmanuelle-Anna Dietz, Ilir Kola and Steffen Hölldobler. Two-Valued Logic is Not Sufficient to Model Human Reasoning, but Three-Valued Logic is: A Formal Analysis
    Abstract: There is an ongoing debate in the psychology of reasoning whether and how logic can be used to describe the human inference process. Many psy- chological findings indicate that humans deviate from classical logic inferences. Some researchers have proposed to use ternary logics instead to model human reasoning processes. In this article we re-analyze the famous Wason Selection Task that has been re- searched in more than 100 publications and can be regarded as one of the most important reasoning experiment in the psychology of reasoning. It investigates how participants check if a given conditional statement holds. Most cognitive modeling approaches have focused on explaining the general response pattern. Instead, we focus on the pattern generated by each participant. In particular, we conduct a meta-analysis to identify these patterns. Thereafter, we analyze these patterns. If there is a two-valued model of human reasoning pro- cesses, then there must be two-valued truth-tables that can generate the patterns. Finally, we show by a search through the space of all two-valued truth tables that there are patterns that cannot be explained by two-valued logics. However, these patterns can be explained, when extending the representation to three-valued log- ics.
    Antonis Kakas, Loizos Michael and Francesca Toni. Argumentation: Reconciling Human and Automated Reasoning
    Abstract: We study how using argumentation as an alternative foun- dation for logic gives a framework in which we can reconcile human and automated reasoning. Logical reasoning, seen from the viewpoint of di- alectic argumentation rather than as a truth preserving process, can give an alternative formulation of formal logic, that on the hand behaves as classical reasoning in strict, scientific domains, but is sufficiently versa- tile to give an automated form of ordinary common sense reasoning, thus offering a way to reconcile and bridge scientific and natural intelligence. We will present this reconciliation between human and automated rea- soning at three levels: (1) at the level of classical strict reasoning on which till today automated reasoning and computing is based, (2) at the level of natural or ordinary human level reasoning as studied in Cog- nitive Psychology and which Artificial Intelligence, albeit in its early stages, has endeavored to automate, and (3) at the level of a computing paradigm with the recent emergence of Cognitive Computing where sys- tems are required to be cognitively compatible to human reasoning based on common sense knowledge or expert knowledge, machined learned from unstructured data in corpora over the web or other sources.
    Ulrich Furbach, Florian Furbach and Christian Freksa. Relating Strong Spatial Cognition to Symbolic Problem Solving --- An Example
    Abstract: In this note, we discuss and analyse a shortest path finding approach using strong spatial cognition. It is compared with a symbolic graph-based algorithm and it is shown that both approaches are similar with respect to structure and complexity. Nevertheless, the strong spatial cognition solution is easy to understand and even pops up immediately when one has to solve the problem.
    Claudia Schon and Ulrich Furbach. Commonsense Reasoning meets Theorem Proving
    Abstract: The area of commonsense reasoning aims at the creation of systems able to simulate the human way of rational thinking. This paper describes the use of automated reasoning methods for tackling commonsense reasoning benchmarks. For this we use a benchmark suite introduced in the literature. Our goal is to use general purpose background knowledge without domain specific hand coding of axioms, such that the approach and the result can be used as well for other domains in mathematics and science. We furthermore report about a preliminary experiment for finding most plausible results.

    Program Overview

    Saturday July 9th, room Nassau West, 2nd floor

    9:00 - 10:30 Welcome
    Invited Talk:
    Sangeet Khemlani:
    Automating Human Inference

    10:30 - 11:00

    Coffee Break

    11:00 - 12:30

    Naveen Sundar Govindarajulu and Selmer Bringsjord:
    Crowdsourcing Theorem Proving via Natural Games
    Aaron Sloman:
    Natural Vision and Mathematics: Seeing Impossibilities

    12:30 - 13:30

    Lunch Break

    13:30 - 15:30

    Ulrich Furbach, Florian Furbach and Christian Freksa:
    Relating Strong Spatial Cognition to Symbolic Problem Solving --- An Example
    Antonis Kakas, Loizos Michael and Francesca Toni:
    Argumentation: Reconciling Human and Automated Reasoning
    Ana Costa, Emmanuelle-Anna Dietz, Steffen Hölldobler and Marco Ragni:
    Syllogistic Reasoning under the Weak Completion Semantics

    15:30 - 16:00

    Coffee Break

    16:00 - 17:30

    Marco Ragni, Emmanuelle-Anna Dietz, Ilir Kola and Steffen Hölldobler:

    Two-Valued Logic is Not Sufficient to Model Human Reasoning, but Three-Valued Logic is: A Formal Analysis
    Ulrich Furbach and Claudia Schon:
    Commonsense Reasoning meets Theorem Proving
    Discussions and closing