Towards a Logical Analysis of Biochemical Pathways
Patrick Doherty, Steve Kertes, Martin Magnusson, and Andrzej Szalas
Department of Computer and Information Science, SE-581 83 Linköping, Sweden,
email: {patdo,g-steke,marma,andsz}@ida.liu.se

Abstract. Biochemical pathways or networks are generic representations used
to model many different types of complex functional and physical interactions inbiological systems. Models based on experimental results are often incomplete,e.g., reactions may be missing and only some products are observed. In suchcases, one would like to reason about incomplete network representations andpropose candidate hypotheses, which when represented as additional reactions,substrates, products, would complete the network and provide causal explanations for the existing observations.
In this paper, we provide a logical model of biochemical pathways and show
how abductive hypothesis generation may be used to provide additional information about incomplete pathways. Hypothesis generation is achieved using weakest
and strongest necessary conditions which represent these incomplete biochemical
pathways and explain observations about the functional and physical interactions
being modeled. The techniques are demonstrated using metabolism and molecular synthesis examples.

Keywords: abduction, biochemical pathways, hypotheses generation, weakest sufficient and strongest necessary conditions

1 Introduction
Biochemical pathways or networks are generic representations used to model manydifferent types of complex functional and physical interactions in biological systems.
For example, metabolism can be viewed and modeled in terms of complex networks ofchemical reactions catalyzed by enzymes and consisting of reactive chains of substrates
and products (see, e.g., [1, 2]).
Often these models are incomplete. For example, reactions may be missing and only
some products are observed. In such cases, one would like to reason about incomplete
network representations and propose candidate hypotheses, which when represented asadditional reactions, substrates, products, or constraints on such, would complete the
network and provide causal explanations for the existing observations.
In this paper, we provide a logical model of biochemical pathways (Section 2) andshow how abductive hypothesis generation may be used to provide additional information about incomplete pathways. Hypothesis generation is achieved using weakest
and strongest necessary conditions for restricted fragments of 1st-order theories which
represent these incomplete biochemical pathways and explain observations about the

2

P. Doherty, S. Kertes, M. Magnusson, A. Szalas

functional and physical interactions being modeled (see Section 3). Quantifier elimination techniques (see [3–5]) are used to automatically generate these hypotheses, using
the technique described in [6].
Part of the modeling process includes the use of approximate databases [7], where
when queries are viewed as inferences, questions can be asked about the generated
hypotheses (see Section 4).
These techniques are demonstrated in Section 5, using metabolism and molecularsynthesis examples.
Comparing to other approaches, e.g., that presented in [8, 9], we focus on modeling reactions in the classical first-order logic and then on hypotheses generation, using
approximations provided by strongest necessary and weakest sufficient conditions, andon evaluation of queries using approximate databases, where queries are tractable.
This paper is an extended version of extended abstract [10].

2 Data Models for the Analysis of Biochemical Pathways
2.1 Preliminaries
The analysis of biochemical pathways has been considered in numerous papers (see,e,g, [1, 2]). In this paper, a bipartite graph representation of chemical reactions will be
used (see, e.g., [2]).
It is assumed that any reaction is specified by:α(n)n : c1 + . . . + ck −→ c1 + . . . + cl ,where:– n is a label (name) of the reaction– c1 , . . . , ck are reactants (inputs for n)– c1 , . . . , cl are products of n and α(n) is a formula that specifies additional conditions necessary for the reaction, such as temperature, pressure, presence of catalyzers, etc.
In a bipartite graph there are two types of nodes: compound nodes (depicted bycircles) and reaction nodes (depicted by rectangles). An edge from a compound node toa reaction node denotes a substrate. An edge from a reaction node to a compound nodedenotes a product of the reaction. We additionally allow conditions placed in the boxes,
if these are specified for particular reactions (see Figure 1).
2.2 Representing Reactions in Logic
The language In the paper, the classical first-order logic is used for specifying reactions.
Reaction nodes will be represented explicitly, while information about available
compounds will be given via a suitable relation. Consequently, it is assumed that thefollowing symbols are available:

Towards a Logical Analysis of Biochemical Pathwaysc1αn1 : c1 + c2 −→ c3
n2 : c3 → c4

c2

n1

s α
*

3

n2

- c3

-

- c4

n3
c1

n3 : c1 −→ c3

-

j

γ

n4 : c2 −→ c3c2n5 : c3 −→ c4

- γ

*

n5
c3

-

- c4

n4
Fig. 1. Examples of bipartite graphs.

1. constants and variables:– constants representing (naming) reactions (denoted by n, n  ), compounds (denoted by c, c  , h2o, co2 etc.), and reaction nodes (denoted by r, r  )– variables representing reactions, denoted by N, N  , compounds (C, C  ), andreaction nodes (R, R  );for constants and variables we also use indices, when necessary
2. relation symbols reflecting static information:– in(C, N ) meaning that compound C is needed for reaction N– out(N, C) meaning that compound C is a product of reaction N
3. relation symbols reflecting dynamic information:– prec(R, R ) meaning that reaction node R precedes reaction node R – notExcl(R, R ) meaning that precedence prec(R, R  ) is not excluded 1– chain(R, R ) meaning that there is a chain of reactions R, R 1 , R2 , . . . , Rk , Rsuch that prec(R, R1 ), prec(R1 , R2 ), . . . ,prec(Rk−1 , Rk ), prec(Rk , R )– react(N, R) meaning that reaction N actually happened in reaction node R– av(C, R) meaning that compound C is available for reaction represented byreaction node R.
Specifying Reactions in Logic Let e, t be any expressions and s any subexpressionof e. By e(s/t) we shall mean the expression obtained from e by substituting eachoccurrence of s by t.
It is assumed that any formula is implicitly universally quantified over all its variables that are not bound by a quantifier.
Any reaction of the formα(n)n : c1 + . . . + ck −→ c1 + . . . + cl ,(1)is translated into the formula react(n, R), where the following integrity constraints are
assumed:1

notExcl(R, R ) is useful for constraining the hypothesis generation process.

4

P. Doherty, S. Kertes, M. Magnusson, A. Szalas– static information about reaction n:in(c1 , n) ∧ . . . ∧ in(ck , n)∧out(n, c1 ) ∧ . . . ∧ out(n, cl )– linking nodes in graphs with reactions
react(n, R) →(2)α(n/R)∧∀C. {in(C, n) → av(C, R)}∧∀R , C  . {[prec(R, R ) ∧ out(n, C  )] → av(C  , R )}.
Observe that the above formula can be more efficiently expressed according to theschema:react(n, R) →α(n/R)∧(3)

av(c1 , R) ∧ . . . ∧ av(ck , R)∧∀R . {prec(R, R ) → av(c1 , R )}∧...∧∀R . {prec(R, R ) → av(cl , R )}.
However, in order to link to an existing biochemical database one would most probably have to use the previous version with suitable syntactic adjustments.

3 Strongest Necessary and Weakest Sufficient Conditions
3.1 Preliminaries
The strongest necessary and weakest sufficient conditions, as understood in this paperand defined below, have been introduced in [11] and further developed in [6]. Observethat the weakest sufficient condition corresponds to the weakest abduction expressed interms of a chosen vocabulary.
Definition 3.1. By a necessary condition of a formula α on the set of relation symbols
P under theory T we shall understand any formula φ containing only symbols in P suchthat T |= α → φ. It is the strongest necessary condition, denoted by S NC (α; T ; P ) if,
additionally, for any necessary condition ψ of α on P under T , T |= φ → ψ holds. 2
Definition 3.2. By a sufficient condition of a formula α on the set of relation symbols
P under theory T we shall understand any formula φ containing only symbols in P
such that T |= φ → α. It is the weakest sufficient condition, denoted by W SC (α; T ; P )if, additionally, for any sufficient condition ψ of α on P under T , T |= ψ → φ holds. 2
The set P in the definitions for wsc’s and snc’s is referred to as the target language.
The following lemma has been proven in [6].

Towards a Logical Analysis of Biochemical Pathways

5

Lemma 3.3. For any formula α, any set of relation symbols P and theory T such thatthe set of free variables of T is disjoint with the set of free variables of α:
S NC(α; T ; P ) ≡ ∃Φ̄. [T ∧ α]

(4)

W SC (α; T ; P ) ≡ ∀Φ̄. [T → α],(5)where Φ̄ consists of all relation symbols appearing in T and α but not in P .

2The above characterizations are second-order. However, for a large class of formulas, one can obtain logically equivalent first-order formulas 2 (see, e.g., [3, 4]) or
fixpoint formulas 3 (see, e.g., [5]) by applying techniques for eliminating second-order
quantifiers. The algorithms given in [3, 4] are implemented and are available online.
The algorithm based on [5] is implemented, as described in Section 4.
3.2 Hypotheses Generation Using Snc’s and Wsc’s
Snc’s and Wsc’s provide a powerful means of generating hypotheses using abduction.
Suppose one is given a (incomplete) specification of a set of interacting reactions of theform shown in equation (1). We would use this set of formulas as the background theory
T . Suppose additionally, that a number of observations are made referring to reactions
known to have occurred, or compounds known to be available for participation in areaction, etc. Let α denote the formula representing these observations. Generally, it
will not be the case that T |= α because T only provides an incomplete specification of
the reactions.
We would like to generate a formula ( candidate hypotheses) φ in a restricted subsetof the language of reactions P such that φ together with the background theory T does
entail the observations α. It is important that we do not over commit otherwise we could
just as easily choose α itself as the hypothesis which wouldn’t do much good. In fact,
the W SC (α; T ; P ) does just the right thing since we know that T ∧ W SC (α; T ; P ) |= αand it is the weakest such formula by definition.
W SC (α; T ; P ) actually represents alternative hypotheses for explaining α. If it isput in disjunctive normal form, each of the disjuncts makes W SC (α; T ; P ) true andrepresents a weakest hypothesis. To reason about what each candidate hypothesis might
imply in terms of completing the reaction representation, one would simply add boththe background theory T and the candidate hypothesis α  to the approximate database
described in Section 4 and query the database as desired.
Technically, if the wsc/sns in question can be expressed using the classical firstorder logic, 4 one would then perform the following steps:
1. replace any quantifier ∀X. α(X) by the conjunction α(X/a 1 ) ∧ . . . ∧ α(X/ak ),where a1 , . . . , ak are all constants occurring in the database of the type compatible
with the type of X
2

The class of formulas includes, e.g., all non-recursive semi-Horn formulas - see, e.g., [12].
Fixpoint formulas are obtained for semi-Horn formulas, a formalism substantially more expressive than the Horn fragment of first-order logic.
4E.g., second-order quantifier elimination results in a first-order formula.
3

6

P. Doherty, S. Kertes, M. Magnusson, A. Szalas

2. replace any quantifier ∃X. α(X) by the disjunction α(X/a 1 ) ∨ . . . ∨ α(X/ak ),where a1 , . . . , ak are as above
3. transform the resulting formula into prenex normal for with the quantifier-free parttransformed into the disjunctive normal form.
Observe that two first steps are of linear complexity wrt size of the database. However,
the third step might be of exponential complexity wrt the size of the formula obtainedin previous steps. One can, however, generate suitable disjuncts one at a time, not all ofthem at once.
Each disjunct is a conjunction of literals and represents a possible set of facts making a given snc or wsc true. It could then be used to update the database containing
the background theory. One could then query database, using the language outlined in
Section 4 in order to verify certain properties of the generated hypotheses (e.g., whether
the obtained chain of reactions is cycle-free or is acceptable by experts).
In the case when the wsc and snc are fixpoint formulas, one can use the standard
characterization of fixpoints as disjunctions/conjunctions of iterations of fixpoint operators. However, the complexity of the resulting formula might in this case be unacceptable.
3.3 Applications of Snc’s and Wsc’s in the Analysis of Biochemical Pathways
Observe that:– wsc corresponds to a weakest abduction expressed in a given target language. For
example, consider
W SC (av(f in, so3); T h; L),
where T h is the theory expressing properties of given reactions, as constructed in
Section 2.2. Then
• if the target language L consists of av only, the resulting wsc expresses what
compounds availability makes the required output of reaction node f in feasible• if the target language consists of react, then the resulting wsc expresses reactions necessary to make the required output of f in feasible– snc allows to infer facts from a negative information. In fact, snc expresses what
would be possible under a given set of hypotheses. For example, if a certain sideproduct has not been observed, a reaction can be excluded from the set of hypotheses.

4 Approximate Databases
4.1 Introduction
An approximate database is based on the standard concept of a deductive database butwith a number of modifications that enable reasoning about incomplete and approximate knowledge.
The basis for the representation of data are approximate relations. An approximate
relation, say R, is given by:

Towards a Logical Analysis of Biochemical Pathways

7– a lower approximation, denoted by R + , containing objects known to satisfy the
relation– an upper approximation, denoted by R ⊕ , containing objects that may satisfy the
relation.
We also allow in the language R − , consisting of tuples which are known not to satisfy
R, R consisting of tuples that may not satisfy R and R ± , called the boundary ofR, consisting of tuples for which it is unknown whether they satisfy R. Of course,
R⊕ = R+ ∪ R± and R = R− ∪ R± .
Queries to the database are approximate formulas, where all relations are approximate. In the case of a query containing free variables, the result of the query is a listof substitutions for those variables that satisfy the query. In the case of a query without
free variables, the result is true, false or unknown.
A prototype implementation of the approximate database management system thatfunctions as a front-end to the P OSTGRE S QL database has been developed. The architecture of implemented layers is depicted in Figure 2.

Semi-Horn theory
Minimization policy
Atomic formula query-

Circumscription

C CQ Database

D LS ∗
Semi-Horn rules
Approximate
fixpoint query*

Intensional database

Inferencemechanism

Extensional databaseQuerycompiler

q

S QL

?
P OSTGRE S QL
Fig. 2. The architecture of the knowledge database.

An extensional database layer (E DB) defines object constants and relations, including information about argument types, and explicitly stores positive (R + ) and negative(R− ) information for each relation R. The Boundaries of any approximate relation canbe generated by combining its explicit information with all possible tuples of constants
constrained by the argument types. A query compilation mechanism translates any approximate fixpoint formula into standard S QL and returns bindings of free variables
using results from the P OSTGRE S QL database.

8

P. Doherty, S. Kertes, M. Magnusson, A. Szalas

An intensional database layer (I DB) contains deductive rules in the form of approximate formula implications and infers new positive or negative information by applying
the inference mechanism on data in the E DB.
Finally, a contextually closed query layer (the C CQ layer) provides functionality
for local closed world assumptions by circumscribing a definition of the query in thecontext of a minimization/variation policy (see, [7]). The circumscription generates asecond order formula, which can often be reduced into a logically equivalent fixpoint
formula that can be evaluated by the E DB. This is achieved through application of the
D LS ∗ algorithm (described, e.g., in [13]).
4.2 Using Approximate Databases for Representing Biochemical Pathways
Bipartite graphs describing chemical reactions can be represented and reasoned about
using queries to an approximate database with the language presented in Section 4.1.
As is often the case, the reaction graph may be incomplete, in which case querying may
be insufficient to draw any conclusions at all. In this case we propose the application of
Wsc’s and Snc’s in order to hypothesize additional reaction pathways before querying.
According to the definitions of Wsc’s and Snc’s they are equivalent to second orderformulas. Using the D LS ∗ algorithm, which is part of the C CQ layer, these can often be
reduced into equivalent first order of fixpoint formulas.
When a hypothesis has been generated, as described in Section 3.2, it can be added
to the database together with the background theory and initial conditions regarding theavailability of compounds. Any consequences of the hypothesis can then be investigatedby querying the database.
For example one might want to find compounds that are available as a result of thereactions in the hypothesis by performing the query:∃N, R [react+ (N, R) ∧ out+ (N, C)].
The compound variable C is unbound and the query will return any compounds that
resulted from any reaction that actually took place. If one of these compounds could
not be found after performing the experiment, this might be a reason to exclude thehypothesis.
Consider now relations described in Section 2.2.
We assume that relations in and out are in the knowledge database or, alternatively,that the database contains definitions of reactions prepared according to schema (2) or(3) (see Section 2.2). In what follows we assume for simplicity that schema (3) is usedwhenever possible.
Relations prec, chain, react and av are often known only partially on the basis ofobservations. In such a case, in order to find the missing information, we will projectout those relation symbols using the methodology of approximations based on weakest sufficient and strongest necessary conditions (see Section 3). We will assume thefollowing set of formulas, reflecting the partial knowledge:– if it is known that react(n, r) holds, where n and r are constants, and n is specifiedby (1), then one adds to the database formula[N = n ∧ R = r] → react+ (N, R)

Towards a Logical Analysis of Biochemical Pathways

9– if prec(r, r ) is known, then one adds formula[R = r ∧ R = r ] → prec+ (R, R ),and similarly for chain– if av(c, r) is known, then one adds formula[C = c ∧ R = r] → av+ (C, R).
If some reaction nodes are missing then one has to make sure that database domain
has some extra constants for such nodes. These constants can eventually be used in
hypothesis generation (see Section 3.2).
One also adds the following formulas:– sufficient condition for prec:∃ C, N. [react+ (N, R) ∧ out+ (N, C)∧




(6)


av+ (C, R ) ∧ notExcl⊕ (R, R )] → prec+ (R, R )– necessary condition for prec
prec+ (R, R ) →∃ C, N. [react+ (N, R) ∧ out+ (N, C) ∧ av+ (C, R )].

(7)

Remark 4.1. All the formulas considered so far allow one to compute weakest sufficient and strongest necessary conditions as classical first order formulas, provided that
additional conditions expressed by formula α in all reactions (see Equation (1)) are2
non-recursive.
The following formulas are sometimes 5 required, but should be avoided wheneverpossible, since computing weakest sufficient and strongest necessary conditions in theirpresence results in fixpoint formulas which are much more complex to handle during
the hypothesis generation stage. 6– definition of chain:defchain+ (R, R ) ≡prec+ (R, R )∨∃R1 . [prec+ (R, R1 ) ∧ chain+ (R1 , R )].
– no cycles:∀R. [¬chain+ (R, R)] (or, alternatively, ∀R. [chain  (R, R)]).
One can also describe the availability of certain compounds and some other conditions. For example, ∀R. [av + (h2so4, R)] specifies that H2SO4 is known to be available for any reaction node.
5
6

When the reasoning concerns chains of reactions of not bounded a priori length .
In fact, from the point of view of complexity, it is better to use these formulas as integrity
constraints to rule out certain hypotheses (see discussion in Section 3.2).

10

P. Doherty, S. Kertes, M. Magnusson, A. Szalas

5 Examples
5.1 A Metabolism Example
Consider a fragment of the aromatic amino acid pathway of yeast, shown in Figure 3(this is a fragment of a larger structure used in [1]). Rectangles are labelled with enzyme
names, meaning that a respective enzyme is to be available for reaction, i.e., that av
holds. For example, av(ydr127w, r) is necessary, when the label of r is “YDR127W”.

C02652

C00006q
1

1
C00493-

YDR127W

C00005C00002*YDR127W

C03175?

R
C00008

YGL148W?

?

C00009C00251?

C01269

YDR127W+
C00009I
C00074

Fig. 3. A fragment of the aromatic amino acid pathway of yeast.

Figure 3 depicts the following reactions:n1 : C02652 + C00005

YDR127W−→

C00006 + C00493

n3 : C03175 + C00074

YDR127W

C01269 + C00009

n4 : C01269

YGL148W−→−→

C00009 + C00251.

It is assumed that reaction
n2 : C00493 + C00002

YDR127W−→

C03175 + C00008

depicted by the dashed box is, in fact, missing.
The above set of reactions is expressed by formulas as defined in Section 2.2. For
example, the first reaction is expressed by:react(n1 , R) →av(ydr127w, R)∧av(c02652, R) ∧ av(c00005, R)∧∀R . [prec(R, R ) → av(c00006, R)]∧∀R . [prec(R, R ) → av(c00493, R)].

Towards a Logical Analysis of Biochemical Pathways

11

The missing reaction is also present, among many other reactions, in the database, andis expressed by:react(n2 , R) →av(ydr127w, R)∧av(c00493, R) ∧ av(c00002, R)∧∀R . [prec(R, R ) → av(c03175, R)]∧∀R . [prec(R, R ) → av(c00008, R)].
We assume that the underlying database contains partial information about the observed
chain of reactions:react(n1 , r1 ) ∧ react(n3 , r3 ) ∧ react(n4 , r4 )together with a description of reactions n 1 , n3 , n4 and many other reactions, including
n3 . Let the considered knowledge base be denoted by K DB. We assume, for simplicity,that no precedence of reactions is excluded, ∀R, R . notExcl⊕ (R, R ).
We can now consider, e.g., W SC (α; K DB; av), wheredef

α ≡ ∃N.[react(N, r2 ) ∧ prec(r1 , r2 ) ∧ prec(r2 , r3 )],providing one with the weakest requirement expressed in terms of av only, making α
true, provided that the background theory given by K DB holds.
In our case, the generated hypotheses will contain the disjunct av + (c00002, r2),
reflecting, among others, sufficient conditions for prec, expressed by (6).
The S NC (α; K DB;{out}) will contain the disjunctout+ (N, c03175) ∧ out+ (N, c00008),
reflecting, among others, necessary conditions for prec, expressed by (7). If one of thecompounds c03175, c00008 has not been observed during the reaction chain, one canreject the hypothesis that reaction N in node r 2 was n2 .
5.2 Synthesis of 3-bromo-4propylphenol from Benzene
This example shows how to express additional conditions on reactions.
Consider the following reactions for synthesis of 3-bromo-4propylphenol from benzene (see [14]): 7
n1: C6H6 + C3H5OCl + AlCl3 −→ C9H10O
n2: C9H10O + Zn(H5) + HCl −→ C8H12
n3: C9H12 + HNO3 + H2SO4 −→ C9H11NO2
n4: C9H11NO2 + Br2 + FeBr3 −→ C9H10NO2Br
n5: C9H10NO2Br + Sn + HCl −→ C9H12NBr
n6: C9H12NBr+NaNO2+H2SO4+H2O

0o C+heat−→

C9H11OBrIn order to express the condition “0 o C + heat”, one has to extend the language byadding the following relations:7

The condition in reaction n6 is intended to mean that the reaction has to start at a temperatureof 0o C and then the reactants are to be heated.

12

P. Doherty, S. Kertes, M. Magnusson, A. Szalas– temp(R, T ) meaning that the temperature in node R is initially T– heat(R) meaning that compounds in node R are heated.
Now “0o C + heat” is expressed by temp(R, 0) ∧ heat(R) and the reaction n 6 is expressed by:react(n6 , R) →temp(R, 0) ∧ heat(R)∧av(c9h12nbr, R) ∧ av(nano2, R)∧av(h2so4, R) ∧ av(h2o, R)∧∀R . [prec(R, R ) → av(c9h11obr, R)].
The hypotheses generated here might also have to be expressed in terms of a richer
language. For example, the weakest sufficient condition for reaction n 6 to react in node
r would involve temp(r, 0) ∧ heat(R). In fact, no condition expressed in terms of
relations introduced in Section 2.2 would make n 6 feasible, since none of them implies
temp(r, 0) or heat(R).

6 Conclusions
In the paper we have presented a logical model of biochemical pathways and haveshown how abductive hypothesis generation may be used to provide additional information about incomplete pathways. Hypothesis generation is achieved using weakest
and strongest necessary conditions which explain observations about the functional andphysical interactions being modeled.
The language for expressing knowledge about biochemical pathways that permits
second-order quantifier elimination is quite broad and includes semi-Horn formulas(see [12]), a formalism substantially more expressive than the Horn fragment of thefirst-order logic. However, if one uses non-recursive semi-Horn formulas, the resulting
formalism is much more efficient.
One can extend the approach in various directions. In particular, one can model
much more complicated conditions required for reactions as well as time dependencies.
The approximate database implementation as well as our earlier work on snc’s andwsc’s has been supported in part by the WITAS project grant under the Wallenberg
Foundation, Sweden.

References
1. Bryant, C., Muggleton, S., Oliver, S., Kell, D., Reiser, P., King, R.: Combining inductive
logic programming, active learning and robotics to discover the function of genes. Linkoping
Electronic Articles in Computer and Information Science 6 (2001)
2. Deville, Y., Gilbert, D., van Helden, J., Wodak, S.: An overview of data models for the
analysis of biochemical pathways. Briefings in Bioinformatics 4 (2003) 246–259
3. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited. Journal ofAutomated Reasoning 18 (1997) 297–336

Towards a Logical Analysis of Biochemical Pathways

13

4. Gabbay, D.M., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In
Nebel, B., Rich, C., Swartout, W., eds.: Principles of Knowledge Representation and Reasoning, KR 92. (1992) 425–435
5. Nonnengart, A., Szałas, A.: A fixpoint approach to second-order quantifier elimination withapplications to correspondence theory. In Orłowska, E., ed.: Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa, Springer Physica-Verlag (1998) 307–328
6. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing strongest necessary and weakest sufficient conditions of first-order formulas. International Joint Conference on AI (IJCAI’2001)(2000) 145 – 151
7. Doherty, P., Kachniarz, J., Szałas, A.: Using contextually closed queries for local closedworld reasoning in rough knowledge databases. In Pal, S., Polkowski, L., Skowron, A., eds.:
Rough-Neuro Computing: Techniques for Computing with Words. Cognitive Technologies,
Springer–Verlag (2003) 219–250
8. Chabrier, N., Fages, F.: Symbolic model checking of biochemical networks. In: Proceedings of the First International Workshop on Computational Methods in Systems Biology
CMSB’03. Volume 2602 of LNCS., Springer-Verlag (2004) 149–162
9. Chabrier-Rivier, N., Fages, F., Soliman, S.: The biochemical abstract machine BIOCHAM. In:
Proceedings of the Second International Workshop on Computational Methods in Systems
Biology CMSB’04. LNCS, Springer-Verlag (2004)
10. Doherty, P., Kertes, S., Magnusson, M., Szałas, A.: Towards a logical analysis of biochemical
pathways (extended abstract). In: Proceedings of the European Conference on Artificial
Intelligence ECAI’2004. (2004) to appear.
11. Lin, F.: On strongest necessary and weakest sufficient conditions. In Cohn, A., Giunchiglia,
F., Selman, B., eds.: Principles of Knowledge Representation and Reasoning, KR’2000.
(2000) 167–175
12. Doherty, P., Łukaszewicz, W., Szałas, A.: A reduction result for circumscribed semi-Hornformulas. Fundamenta Informaticae 28 (1996) 261–271
13. Doherty, P., Łukaszewicz, W., Szałas, A.: General domain circumscription and its effective
reductions. Fundamenta Informaticae 36 (1998) 23–55
14. Pine, S., Hendrickson, J., Cram, D., Hammond, G.: Organic Chemistry. McGraw-Hill, Inc.
(1980)