An Algorithm for Generating Arguments in Classical Predicate Logic

Abstract

There are a number of frameworks for modelling argumentation in logic. They incorporate a formal representation of individual arguments and techniques for comparing conflicting arguments. A common assumption for logic-based argumentation is that an argument is a pair 〈Φ,α〉 where Φ is a minimal subset of the knowledgebase such that Φ is consistent and Φ entails the claim α. Different logics provide different definitions for consistency and entailment and hence give us different options for argumentation. An appealing option is classical first-order logic which can express much more complex knowledge than possible with defeasible or classical propositional logics. However the computational viability of using classical first-order logic is an issue. Here we address this issue by using the notion of a connection graph and resolution with unification. We provide a theoretical framework and algorithm for this, together with some theoretical results.