Arnold Binas

KR Conference 2008 Conference Paper

Peer-to-Peer Query Answering with Inconsistent Knowledge

• Arnold Binas
• Sheila A. McIlraith

Decentralized reasoning is receiving increasing attention due to the distributed nature of knowledge on the Web. We address the problem of answering queries to distributed propositional reasoners which may be mutually inconsistent. This paper provides a formal characterization of a prioritized peer-to-peer query answering framework that exploits a priority ordering over the peers, as well as a distributed entailment relation as an extension to established work on argumentation frameworks. We develop decentralized algorithms for computing query answers according to distributed entailment and prove their soundness and completeness. To improve the efficiency of query answering, we propose an ordering heuristic that exploits the peers’ priority ordering and empirically evaluate its effectiveness.

ECAI Conference 2004 Conference Paper

Guiding a Theorem Prover with Soft Constraints

• John K. Slaney
• Arnold Binas
• David Price

AAAI Conference 2004 Short Paper

Semantically Guiding a First-Order Theorem Prover with a Soft Model

• Arnold Binas
• John Slaney

Various versions of our first-order logic theorem prover SCOTT have been developed over the past decade to employ the concept of semantic guidance for improving the underlying system OTTER by McCune. We introduce our latest attempt to speed up OTTER’s proof search, Softie. While the various SCOTTs consulted an ordinary constraint solver to gain information about the problem to be solved, Softie is implemented from scratch and uses a solver capable of handling soft constraints.