WWW.DISSERTATION.XLIBX.INFO
FREE ELECTRONIC LIBRARY - Dissertations, online materials
 
<< HOME
CONTACTS



Pages:   || 2 | 3 | 4 |

«Abstract. In this paper we define a new clausal class, called BU, which can be decided by hyperresolution with splitting. We also consider the ...»

-- [ Page 1 ] --

A New Clausal Class Decidable by

Hyperresolution

Lilia Georgieva1,2, Ullrich Hustadt3, Renate A. Schmidt1,2

1

Department of Computer Science, University of Manchester, UK

{georgiel,schmidt}@cs.man.ac.uk

2

Max-Planck-Institut f¨r Informatik, Saarbr¨cken, Germany

u u

{georgie,schmidt}@mpi-sb.mpg.de

3

Department of Computer Science, University of Liverpool, UK

U.Hustadt@csc.liv.ac.uk

Abstract. In this paper we define a new clausal class, called BU, which

can be decided by hyperresolution with splitting. We also consider the model generation problem for BU and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for BU and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in BU. In addition, we investigate the relationship of BU to other solvable classes.

1 Introduction In recent work [13, 14] we have considered the fragment GF1− of first-order logic which was introduced by Lutz, Sattler, and Tobies [21]. GF1− is a restriction of the guarded fragment which incorporates a variety of modal and description logics via standard or non-standard translations, and can be seen as a generalisa- tion of these logics. In contrast to the guarded fragment [1], GF1− allows for the development of a space-efficient decision procedure. Under the assumption that either (i) there is a bound on the arity of predicate symbols in GF1− formulae, or (ii) that each subformula of a GF1− formula has a bounded number of free variables, the satisfiability problem of GF1− is PSPACE-complete [21], while under identical assumptions the satisfiability problem of the guarded fragment is EXPTIME-complete [15]. Thus, GF1− has the same complexity as the modal and description logics it generalises.

In [13] we have shown that hyperresolution plus splitting provides a decision procedure for GF1−. One of the interesting features of GF1− is that it is one of the few solvable classes where, during the deduction by the resolution decision procedure, derived clauses can contain terms of greater depth than the clauses in the initial set of clauses. In [14] we have shown that a modification of the main procedure of a standard saturation based theorem prover with splitting can pro- vide a polynomial space decision procedure for GF1−. We also describe several solutions to the problem of generating minimal Herbrand models for GF1−.

We thank the referees for helpful comments and suggestions. The work is supported by research grants GR/M36700 and GR/R92035 from the EPSRC, UK.

1 In [13, 14] we have used structural transformation (or definitional form transformation, cf. e.g. [3, 18]), to transform GF1− formulae into clausal form. While it is straightforward to give a schematic characterisation of the resulting sets of clauses, it is much more difficult to state the conditions which an arbitrary set of clauses needs to satisfy so that it shares most or all the properties of the clauses sets we obtain from the definitional form transformation of GF1− formulae.

In this paper we define a new clausal class BU which generalises the set of all clause sets we can obtain from GF1− via the definitional form transformation.

BU is defined such that hyperresolution plus splitting is still a decision procedure.

Since hyperresolution is implemented in many state-of-the-art theorem provers, e.g. Otter, SPASS, and Vampire, this gives a practical decision procedure for the class. We also show that if an input clause set from BU is not refuted, an adequate representation of a model and of a minimal model of the clausal class can be extracted from the information produced by the prover.

A main motivation for studying classes like GF1− and BU is that a variety of expressive modal and description logics can be embedded into them. Expressive modal and description logics have found applications in such varied areas as, for example, verification, program analysis, knowledge representation, deductive data bases and the semantic web. However, there are a number of alternative solvable classes for which the same is true. We will discuss the relationship of BU to some of these alternative classes.

The paper is organised as follows. Section 2 defines the notation used, some basic concepts and a hyperresolution calculus with splitting. The clausal class BU is defined in Section 3, and the relationship of BU to other solvable classes is discussed in Section 4. The applicability of the hyperresolution calculus as a decision procedure for the class, model building by hyperresolution and in particular, minimal model building are investigated in Sections 5 and 6. The final section is the Conclusion.

2 Fundamentals and hyperresolution

Notation. The notational convention is as follows. We use the symbols x, y, z for first-order variables, s, t, u for terms, a, b for constants, f, g, h for functions, P, Q for predicate symbols, A for atoms, L for literals, C for clauses, ϕ, φ, ψ, for formulae, and N for sets of clauses.

An over-line indicates a sequence. An i-sequence is a sequence with i elements.

If s and t are two sequences of terms and X is a set of terms, then the notation s ⊆ t (s ⊆ X) means that every term in s also occurs in t (X). By definition, s = t (s = X) iff s ⊆ t and t ⊆ s (s ⊆ X and every term in X occurs in s). The union of the terms in s and t is denoted by s ∪ t. Given a sequence s of terms, fs (ui ) denotes a sequence of terms of the form f1 (u1 ),..., fk (uk ), where ui ⊆ s for every 1 ≤ i ≤ k.





Terms, literals, clauses and orderings. The term depth dp(t) of a term t, is inductively defined as follows. (i) If t is a variable or a constant, then dp(t) = 1.

2 (ii) If t = f (t1,..., tn ), then dp(t) = 1 + max dp(ti ) | 1 ≤ i ≤ n. The term depth of a literal is defined by the maximal term depth of its arguments, and the term depth of a clause is defined by the maximal term-depth of all literals in it.

A literal is an atomic formula A (a positive literal) or the negation ¬A of an atomic formula A (a negative literal). We regard a clause as a multiset of literals and consider two clauses C and D to be identical if C can be obtained from D by variable renaming. A multiset over a set L is a mapping C from L to the natural numbers. We write L ∈ C if C(L) 0 for a literal L. We use ⊥ to denote the empty clause. A positive (negative) clause contains only positive (negative) literals. The positive (negative) part of a clause is the subclause of all positive (negative) literals. A split component of a clause C ∨ D is a subclause C such that C and D do not have any variables in common, i.e. are variable disjoint. A maximally split (or variable indecomposable) clause cannot be partitioned (or split) into subclauses which do not share variables.

A clause C is said to be range restricted iff the set of variables in the positive part of C is a subset of the set of variables of the negative part of C. A clause set is range restricted iff it contains only range restricted clauses. This means that a positive clause is range restricted only if it is a ground clause.

A strict partial ordering on a set L (i.e. an irreflexive and transitive relation) can be extended to an ordering mul on (finite) multisets over L as follows:

C mul D if (i) C = D and (ii) whenever D(x) C(x) then C(y) D(y), for some y x. mul is called the multiset extension of.

Given an ordering on literals we define a maximal literal in a clause in the standard way: A literal L in a clause C is maximal in C, if there is no literal L in C, for which L L. A literal L is strictly maximal in C if it is the only maximal literal in C.

A term, an atom, a literal or a clause is called functional if it contains a constant or a function symbol, and non-functional, otherwise.

–  –  –

3 A derivation in Rhyp from a set of clauses N is a finitely branching, ordered tree T with root N and nodes which are sets of clauses. The tree is constructed by applications of the expansion rules to the leaves. We assume that no hyperresolution or factoring inference is computed twice on the same branch of the derivation. Any path N (= N0 ), N1,... in a derivation T is called a closed branch in T iff the clause set j≥0 Nj contains the empty clause, otherwise it is called an open branch. We call a branch B in a derivation tree complete (with respect to Rhyp ) iff no new successor nodes can be added to the endpoint of B by Rhyp, otherwise it is called an incomplete branch. A derivation T is a refutation iff every path N (= N0 ), N1,... in it is a closed branch, otherwise it is called an open derivation.

In general, the calculus Rhyp can be enhanced with standard simplification rules such as tautology deletion and subsumption deletion, in fact, it can be enhanced by any simplification rules which are compatible with a general notion of redundancy [4, 5]. A set N of clauses is saturated up to redundancy with respect to a particular refinement of resolution if the conclusion of every inference from non-redundant premises in N is either contained in N, or else is redundant in N.

A derivation T from N is called fair if for any path N (= N0 ), N1,... in T, with limit N∞ = j≥0 k≥j Nk, it is the case that each clause C which can be deduced from non-redundant premises in N∞ is contained in some Nj. Intuitively, fairness means that no non-redundant inferences are delayed indefinitely. For a finite complete branch N (= N0 ), N1,... Nn, the limit N∞ is equal to Nn.

Theorem 1 ([5]). Let T be a fair Rhyp derivation from a set N of clauses.

Then: (i) If N (= N0 ), N1,... is a path with limit N∞, then N∞ is saturated (up to redundancy). (ii) N is satisfiable if and only if there exists a path in T with limit N∞ such that N∞ is satisfiable. (iii) N is unsatisfiable if and only if for every path N (= N0 ), N1,... the clause set j≥0 Nj contains the empty clause.

The clausal class BU3

The language of BU is that of first-order clausal logic. Additionally, each predicate symbol P is uniquely associated with a pair (i, j) of non-negative integers, such that if the arity of P is n then i + j = n. The pair is called the grouping of the predicate symbol. Sometimes the grouping (i, j) of a predicate symbol P will be made explicit by writing P (i,j). The notion of grouping is extended to literals in the following way. A literal L is said to satisfy the grouping condition with respect to the sequences x and s, if L = (¬)P (i,j) (x, s) or L = (¬)P (j,i) (s, x), where x is an i-sequence of variables, and s is either a j-sequence of variables disjoint from x or a j-sequence of terms of the form f (z) where z ⊆ x, and x is non-empty. Repetitions of variables and terms in any of the sequences are allowed.

Furthermore, an acyclic relation d, called an acyclic dependency relation, is defined over the predicate symbols. Let + be the transitive closure of d. Then d + d is an ordering on predicate symbols. This ordering extends to atoms, literals 4 and clauses by the following definitions. Given two literals L1 = (¬)P1 (s) and L2 = (¬)P2 (t), L1 D L2 iff P1 + P2. The multiset extension of the ordering d D, also denoted by D, defines an ordering on ground clauses. The acyclicity of d implies that D is also acyclic.

Given a finite signature Σ such that (i) any predicate symbol has a unique grouping, and (ii) there is an acyclic dependency relationship d on the predicate symbols in Σ, we define the class BU of clausal sets over Σ as follows.

A clausal set N belongs to BU if any clause C in N satisfies one of the three conditions below as well as the following. If C is a non-ground and non-positive clause then C is required to contain a strictly D -maximal literal, which is negative and non-functional. This literal is called the main literal of the clause.

The predicate symbol P of the main literal must either have the grouping (0, i) or (i, 0), where i is the arity of P.

Condition 1: C is a non-positive, non-ground and non-functional clause and the following is true.

(a) The union of the variables of the negative part can be partitioned into two disjoint subsets X and Y, at least one of which is non-empty.

(b) For every literal L in C, either the variables of L are (i) subsets of X, or (ii) subsets of Y, or (iii) there are non-empty sequences x, y, such that x ⊆ X, y ⊆ Y and L satisfies the grouping condition with respect to x and y.

(c) Either the main literal contains all the variables of the clause, or it contains all the variables from one of the sets X and Y, and there is a negative literal L whose arguments satisfy (b.iii) and which contains all the variables from Y if the main literal contains all the variables from X, or all the variables from X if the main literal contains all the variables from Y.

Condition 2: C is a non-positive and non-ground functional clause and the following is true.

(a) The main literal of C contains all the variables of C.

(b) Every other literal L in C satisfies the grouping condition with respect to two disjoint sequences of variables x and y, or with respect to two sequences x and fx (ui ), where x is a sequence of variables and fx (ui ) is a sequence of terms fi (ui ) such that ui ⊆ x.

Condition 3: C is a positive ground unit clause, its arguments are constants and its predicate symbol has grouping (0, i) or (i, 0).

Consider the following clauses.

1. ¬P (x, y) ∨ ¬Q(x) ∨ ¬R(x, x, y, z) 5. ¬P (x, y) ∨ Q(x, x, y, f (x, y))

2. ¬P (x, y, z) ∨ ¬Q(y, x) ∨ R(x, x, y, z) 6. ¬P (x, y) ∨ Q(x, x, y, g(y))

3. ¬P (x, y) ∨ ¬Q(y, z) ∨ ¬R(x, x, y, z) 7. ¬P (x, y) ∨ Q(x, x, g(y), y)

4. ¬P (x, y) ∨ ¬Q(y, z) ∨ ¬R(x, y, z, x) 8. ¬P (x) ∨ P (f (x)) It follows from the definition of BU that all non-positive clauses must contain a covering negative literal which contains all the variables of the clause. This negative literal can be the main literal, or it is a literal satisfying Condition 1.(b.iii).

5 In the latter case the clause must contain another negative literal which is the main literal. In Clause 1 the literal ¬R(x, x, y, z) is the covering negative literal.



Pages:   || 2 | 3 | 4 |


Similar works:

«Distribution Agreement In presenting this thesis or dissertation as a partial fulfillment of the requirements for an advanced degree from Emory University, I hereby grant to Emory University and its agents the non-exclusive license to archive, make accessible, and display my thesis or dissertation in whole or in part in all forms of media, now or hereafter known, including display on the world wide web. I understand that I may select some access restrictions as part of the online submission of...»

«News Release for the Human Smile ATTN: Members of the Press April 23, 2012 The much-anticipated landmark of the Harajuku/Omotesando area reopens this summer!! Grand opening of the newly renovated KIDDY LAND Harajuku on Sunday, July 1, 2012 ~”SNOOPY Town Shop Harajuku” and “Rilakkuma Store Harajuku” will also be opening~ KIDDY LAND Co., Ltd. KIDDY LAND Co., Ltd. (President and CEO: Yukio Shoji; Headquarters: Taito City, Tokyo) is proud to announce the grand opening of its flagship KIDDY...»

«The Education of William Gibbons1 By Scott Nesbit On the afternoon of Friday, July 2, 1886, the “First Colored” church of Charlottesville was “packed to suffocation.”2 Torrential rains had turned the unpaved West Main Street into a mud field, and the church sanctuary abutting the street was thick with steam from the drenched congregation inside, which consisted of much of the town’s African American community and more than a few local whites, as well.3 Rev. William Gibbons’ body had...»

«Writers House London 2016 Rights Guide Adult Titles 21 West 26th Street, New York, NY 10010 USA Tel: (212) 685-2400 Writers House London 2016 OVERSEAS REPRESENTATIVES Baltic States: ANA Baltics Brazil: Agencia Riff Bulgaria: Anthea Literary Agency Czech Republic and Slovakia: Petra Tobiskova, ANA France: Agence Eliane Benisti Germany: Thomas Schlück Literary Agency Greece: JLM Literary Agency Hungary: Judit Hermann, ANA Indonesia: Maxima Creative Agency Israel: The Book Publishers Association...»

«The Cancer Association of South Africa (CANSA) Fact Sheet on Squamous Cell Carcinoma Introduction There are two main categories of skin cancer, namely melanomas and nonmelanoma skin cancers. Squamous cell carcinoma is one of the non-melanoma skin cancers (British Skin Foundation). Squamous Cell Carcinoma (SCC) is a type of carcinoma that arises from squamous epithelium. It is the second most common form of skin cancer in South Africa. It is also sometimes referred to as cancroid. [Picture...»

«ESTUDIO CUATRO MILLONES DE POBRES EN CHILE: ACTUALIZANDO LA LÍNEA DE POBREZA* Felipe Larraín Bascuñán Para medir la pobreza, en Chile se aplica el método de la Canasta de Satisfacción de Necesidades Básicas. Su base es una canasta mínima de alimentación y un factor multiplicador que entrega el costo total de satisfacer las necesidades mínimas alimentarias y no alimentarias. El valor resultante se compara con el ingreso familiar. De acuerdo a las cifras oficiales, la pobreza se habría...»

«Aalto University publication series DOCTORAL DISSERTATIONS 100/2014 Thermodynamic stabilities of complex phases and their assemblages in Ag-Te, Ag-Bi-S and Ag-Cu-S systems Fiseha Tesfaye A doctoral dissertation completed for the degree of Doctor of Science (Technology) to be defended, with the permission of the Aalto University School of Chemical Technology, at a public examination held at the lecture hall V1 of the school (Espoo, Finland) on August 15th 2014 at noon. Aalto University School of...»

«2014-2373 2014-08-13 HACCO, INC. COMMERCIAL 110 Hopkins Drive NET CONTENTS: 50 g Place Pack s Randolph, WI 53956 READ THE LABEL AND CARTON BEFORE USING Tel: 1-920-326-5141 REGISTRATION NO: 31137 PEST CONTROL PRODUCTS ACT Havoc Rodenticide Bait Packs (Pellets) Kills Rats and Mice WARNING SKULL/BONES POISON Warning, contains the allergen wheat. GUARANTEE: Brodifacoum.0.005% Only to be us ed by certified pest control operators, farm ers and pers ons authorized in government-approved pes t...»

«30: 1. The number of speaker points you thought you should get. 2. The number of speaker points you didn’t get. 3. The number of speaker points given to both teams in the down-four bracket by judges who, in their own debating careers, spent a lot of time in the down-four bracket. a priori argument: 1. An argument that bears no relationship to the concept of a priori, but is rather something you expect the judge to accept without your having to prove it. Let's face it: Kant only came up with...»

«Thailand’s Lengthening Roadmap to Elections Asia Report N°274 | 10 December 2015 International Crisis Group Headquarters Avenue Louise 149 1050 Brussels, Belgium Tel: +32 2 502 90 38 Fax: +32 2 502 50 38 brussels@crisisgroup.org Table of Contents Executive Summary I.  Introduction II.  Road to the Roadmap III.  Drafting the Twentieth Constitution A.  First Draft B.  Roadmap Dead Ends IV.  The Road Ahead A.  Revised Roadmap B.  Incipient Praetorianism? C.  Economic Factors D. ...»

«Rocky Mountain PBS Volunteer Bulletin November 2015—Gobble, Gobble Welcome to the November 2015 issue of the Volunteer Bulletin. Your mustread volunteer news arrives early in the month by email, bringing you Rocky Mountain PBS volunteer opportunities, news, history and events of interest. We welcome your comments, feedback and ideas! Email us at VolunteerBulletin@rmpbs.org. Rocky Mountain PBS often uses volunteer photos online, on TV, and on our social media sites to help show the positive...»

«Academic Freedom: In Justification of a Universal Ideal Terence Karran Centre for Educational Research and Development, University of Lincoln, LN6 7TS UK. Email: tkarran@lincoln.ac.uk [This is an electronic version of an article published in the journal Studies in Higher Education ‘Academic Freedom: In Defence of a Universal Ideal’ Studies in Higher Education, Vol. 34, No. 2. Studies in Higher Education is available online at: http://www.informaworld.com] Dr Terence Karran works in Centre...»





 
<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.