Biomedical Engineering Reference
In-Depth Information
words, it does not exist any non-negative integer vector .y
1
;y
2
;:::;y
n
/
tr
2 Z
C
verifying the following equation.
j
b
0
b
00
jD
y
1
.a
1
c
a
/
C
y
2
.a
2
c
a
/
CC
y
n
.a
n
c
a
/
˙
2ı
Therefore, incompatibility clauses of the following form are added for all the
couples of incompatible variables x
b
0
and x
b
00
.
.
:
x
b
0
_:
x
b
00
/
Another set of rules that should be considered in order to have a coherent interpre-
tation is that of
multicharge
rules. Depending on the mass spectrometry device, ions
retaining more than one electrical charge, called multicharged ions, are usually less
common than single charged ions, and it is common practice to assume that if a
multicharged ion has been observed in the spectrum, also the corresponding single
charged one should appear in the spectrum. Therefore, each variable x
j
0
!t;e
with
e>1implies, if it exists, another variable x
j
00
!t;1
with .j
0
c
0
e/e
D
j
00
c
0
,as
follows:
.
:
x
j
0
!t;e
_
x
j
00
!t;1
/
Finally, a number of additional clauses representing a priori known information
about the specific mass spectrometry device used for the analysis, about the ana-
lyzed compound or about other possibly known relations among the interpretations
of the various peaks may also be generated. This is because, clearly, the more
information can be introduced by means of clauses, the more reliable the results of
the analysis will be.
By assuming no limitations on the structure of the generated clauses, therefore
allowing the full expressive power of propositional logic, we obtain at this point
asetof
v
clauses C
1
;C
2
;:::;C
v
. Generally, incompatibility clauses are by far the
more numerous. Since all clauses must be considered together, we construct their
conjunction, that is a generic propositional formula
F
in
conjunctive normal form
(CNF)
F
D
C
1
^
C
2
^^
C
v
Each truth assignment
f
True,False
g
for the variables x
j !t;e
, with j
2
F; t
2
T;
2
E, such that
F
F
e
evaluates to
True
is known as a
model
of
.Wenowhavethe
following result.
Theorem 1.1.
Each model
of the generated propositional formula
corre-
sponds to a coherent solution of the peak interpretation problem for the peptide
under analysis. Moreover, no coherent solution of the peak interpretation problem
which does not corresponds to a model
of
F
can exist.
Proof.
The proof relies on the fact that the formula
F
contains by construction
all the rules (peak assignment rules, incompatibility rules, multicharge rules) that a
peak's interpretation must satisfy to be considered coherent. Therefore, each model
F
Search WWH ::
Custom Search