Abstracts (some are missing)

A. Riazanov, Implementing an Efficient Theorem Prover, PhD thesis, The University of Manchester, 2003

Abstract

Since the invention of resolution and paramodulation calculi, theoretical research in the area of resolution-based theorem proving has achieved a remarkable progress in constructing inference systems based on various refinements of these calculi. The developed theory has a significant but not yet fully realised potential for such applications as formal hardware and software development, computer algebra, and assisting human mathematicians. One of the main obstacles to creating a practically valuable technology on the base of the theory is the lack of knowledge of efficient implementation techniques. Attempts of implementing efficient theorem provers constitute the main source of such knowledge. In this thesis we give an account of such an attempt.

We anatomise the design and implementation of our resolution- and superposition-based theorem prover Vampire whose performance has led it to first places in international competitions during the last four years. A high level description of the overall design of the system and the underlying principles is followed by a detailed discussion of a number of key implementation techniques, devised in the course of our study. These include (i) Limited Resource Strategy, a novel adaptive approach to organising saturation process in the presence of a time limit; (ii) a light-weight method for combining saturation with a restricted form of case analysis, called splitting; (iii) a number of novel term indexing techniques for such important and costly operations as forward and backward subsumption and demodulation; and (iv) a technique for efficient checking of ordering constraints on substitutions.

In the first place, this thesis is aimed at developers of deductive software, especially saturation-based theorem provers.  It can also be useful for theorists and people interested in applications of automatic theorem proving wishing to understand the architecture and capabilities of the modern systems.

A. Riazanov and A. Voronkov, The Design and Implementation of Vampire, AI Communications 15:2-3, 2002

Abstract

In this article we describe Vampire: a high-performance theorem prover for first-order logic. As our description is mostly targeted to the developers of such systems and specialists in automated reasoning, it focuses on the design of the system and some key implementation features. We also analyze the performance of the prover at CASC-JC.

A. Riazanov and A. Voronkov, Limited Resource Strategy in Resolution Theorem Proving, Journal of Symbolic Computation, 36:1-2, 2003

Abstract

For most applications of first-order theorem provers a proof should be found within a fixed time limit. When the time limit is set, systems can perform much better by using algorithms other than the ordinary complete ones. In this paper we describe the Limited Resource Strategy intended to improve performance of the OTTER saturation algorithm when a fixed limit is imposed on the time of a run. The strategy is adaptive in the following sense: it adjusts the limit on the weight of clauses according to some statistics collected on the earlier stages of proof search. We give experimental evidence that the Limited Resource Strategy gives a big improvement over the OTTER saturation algorithm. We also show that it is competitive with the DISCOUNT algorithm, which does not use passive clauses for simplification, and the non-adaptive weight-based algorithms.

A. Riazanov and A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, Vol. 199, Issues 1-2, 2005

Abstract

Backward demodulation is a simplification technique used in saturation-based theorem proving with superposition and ordered paramodulation. It requires instance retrieval, i.e., search for instances of some term in a typically large set of terms. Path indexing is a family of indexing techniques that can be used to solve this problem efficiently. We propose a number of powerful optimisations to standard path indexing. We also describe a novel framework, called relational path indexing, which combines path indexing with relational joins. The main advantage of the proposed scheme is flexibility, which we illustrate by sketching how to adapt the scheme to instance retrieval modulo commutativity and backward subsumption on multi-literal clauses.

A. Riazanov and A. Voronkov, Partially Adaptive Code Trees, Proc. JELIA, LNAI 1919, 2000

Abstract

Code trees is an indexing technique used for implementing several indexed operations on terms in the theorem prover Vampire. Code trees offer greater flexibility than discrimination trees. In this paper we review a new, considerably faster, version of code trees based on a different representation of the query term. We also introduce a partially adaptive version of code trees.

A. Riazanov and A. Voronkov, Splitting without Backtracking, Proc. IJCAI-17, vol. 1, 2001

Abstract

Integrating the splitting rule into a saturation-based theorem prover may be highly beneficial for solving certain classes of first-order problems. The use of splitting in the context of saturation-based theorem proving based on explicit case analysis (as implemented in SPASS) employs backtracking which is difficult to implement as it affects design of the whole system. Here we present a cheap'' and efficient technique for implementing splitting that does not use backtracking.

A. Riazanov and A. Voronkov, Adaptive Saturation-Based Reasoning, Proc. PSI 2001, LNCS 2244, 2001

Abstract

We describe the Limited Resource Strategy intended to improve performance of resolution-based theorem provers when a fixed limit is imposed on the time of a run. We give experimental evidence that the Limited Resource Strategy gives a significant improvement over the algorithms not using passive clauses for simplification and the weight-based algorithms.

A. Riazanov and A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Proc. CADE-19, LNAI 2741, 2003

Abstract

Path indexing is a family of indexing techniques that can support instance retrieval, which is the core of any implementation of backward demodulation. We propose a number of powerful optimisations to standard path indexing. We also describe a novel flexible framework, called relational path indexing, that combines path indexing with relational joins. We illustrate the flexibility of relational path indexing by sketching how to adapt the scheme to instance retrieval modulo commutativity and backward subsumption on multi-literal clauses.

A. Riazanov and A. Voronkov, Efficient Checking of Term Ordering Constraints, Proc. IJCAR 2004, LNAI 3097, 2004

Abstract

Simplification orderings on terms play a crucial role in reducing the search space in paramodulation-based theorem proving. Such a use of orderings requires checking simple ordering constraints on substitutions as an essential part of many operations. Due to their frequency, such checks are costly and are a good target for optimisation. In this paper we present an efficient implementation technique for checking constraints in one of the most widely used simplification orderings, the Knuth-Bendix ordering. The technique is based on the idea of run-time algorithm specialisation, which is a close relative of partial evaluation.

D. Tsarkov and A. Riazanov and S. Bechhofer and I. Horrocks, Using Vampire to Reason with OWL, Proc. ISWC 2004, 2004

Abstract

OWL DL corresponds to a Description Logic (DL) that is a fragment of classical first-order predicate logic (FOL). Therefore, the standard methods of automated reasoning for full FOL can potentially be used instead of dedicated DL reasoners to solve OWL DL reasoning tasks. In this paper we report on some experiments designed to explore the feasibility of using existing general-purpose FOL provers to reason with OWL DL. We also extend our approach to SWRL, a proposed rule language extension to OWL.

A. Riazanov, Efficient Semantic Querying of Relational Databases with Resolution, Proc. CSWWS 2009, 2009

Abstract

We address the problem of semantic querying of relational databases (RDB) modulo knowledge bases using very expressive knowledge representation formalisms, such as full first-order logic or its various fragments. We propose to use a first-order logic (FOL) reasoner for computing schematic answers to deductive queries, with the subsequent instantiation of these schematic answers using a conventional relational DBMS. In this paper, we outline the main idea of this technique – using abstractions of databases and constrained clauses for deriving schematic answers. The proposed method can be directly used with regular RDB, including legacy databases. Moreover, we propose it as a potential basis for an efficient Web-scale semantic search technology.

A. Riazanov and M. A. T. Aragao, Incremental Query Rewriting, Canadian Semantic Web: Technologies and Applications, 2010

Abstract

We address the problem of semantic querying of relational databases (RDB) modulo knowledge bases using very expressive knowledge representation formalisms, such as full first-order logic or its various fragments. We propose to use a resolution-based first-order logic (FOL) reasoner for computing schematic answers to deductive queries, with the subsequent translation of these schematic answers to SQL queries which are evaluated using a conventional relational DBMS. We call our method incremental query rewriting, because an original semantic query is rewritten into a (potentially infinite) series of SQL queries. In this chapter, we outline the main idea of our technique – using abstractions of databases and constrained clauses for deriving schematic answers, and provide completeness and soundness proofs to justify the applicability of this technique to the case of resolution for FOL without equality. The proposed method can be directly used with regular RDBs, including legacy databases. Moreover, we propose it as a potential basis for an efficient Web-scale semantic search technology.

A. Riazanov, A. Shaban-Nejad, A. Klein, G. W. Rose, A. J. Forster, D. L. Buckeridge, C. J. O. Baker, Towards Clinical Intelligence with SADI Semantic Web Services: a Case Study with Hospital-Acquired Infections Data, SWAT4LS 2011

Abstract

Clinical Intelligence, as a research and engineering discipline, is dedicated to the development of tools for data analysis for the purposes of clinical research, surveillance and rational health care management. Ad hoc querying of clinical data is one desirable type of functionality. Since most of the data is currently stored in relational or similar form, ad hoc querying is problematic as it requires specialised technical skills and the knowledge of particular data schemas. A possible solution is semantic querying where the user formulates queries in terms of domain ontologies that are much easier to navigate and comprehend than data schemas. Existing approaches to semantic querying of relational data, based on declarative semantic mappings from data schemas to ontologies, such as RDFizing and query rewriting, cannot cope with situations when some computation is required to turn relational data into RDF or OWL, e.~g., to implement temporal reasoning. In this paper, we are exploring the possibility of using \emph{SADI Semantic Web services} for semantic querying of clinical data and report preliminary progress on prototyping a semantic querying infrastructure for the surveillance of, and research on hospital-acquired infections.