The efficiency of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary natureof higher-order unification algorithms, which requires the integration of unification within the calculus and results in a non-efficient search for refutations.We present a modification of the constrained resolution calculus (Huet'72) which uses an eager unification algorithm while retaining completeness. Thealgorithm is complete with regard to bounded unification only, which for many cases, does not pose a problem in practice.
BDI (Bounded Depth Increase) is a new decidablefirst-order clause class. It strictly includesknown classes such as PVD. The arityof function and predicate symbols as well as theshape of atoms is not restricted in BDI. Insteadthe shape of "cycles" in resolution inferences isrestricted such that the depth of generated clausesmay increase but is still finitely bound.The BDI class is motivated by real world problemswhere function terms are used to represent record structures.We show that the hyper-resolution calculus moduloredundancy elimination terminates on BDI clause sets.Employing this result to the ordered resolution calculus,we can also prove termination of ordered resolution on BDI,yielding a more efficient decision procedure.
AbstractWe present novel reductions of the propositional modal logics
"Image missing"
,
"Image missing"
,
"Image missing"
,
"Image missing"
and
"Image missing"
to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover
"Image missing"
to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover
"Image missing"
performs well when compared with a specialised resolution calculus for these logics and with the b̆uilt-in reductions of the first-order prover SPASS.
Abstract
Hoerl and McCormack demonstrate that although animals possess a sophisticated temporal updating system, there is no evidence that they also possess a temporal reasoning system. This important case study is directly related to the broader claim that although animals are manifestly capable of first-order (perceptually-based) relational reasoning, they lack the capacity for higher-order, role-based relational reasoning. We argue this distinction applies to all domains of cognition.
A Resolution Calculus for Second-order Logic with Eager Unification