Is there a standard quantifier notation for an exact number of true values?
1
$begingroup$
When working with SAT Solvers, I need to write quantifiers that give the total number of true values. The usual quantitiers $forall$ and $exists$ do not suffice. Is there a standard notation for writing the following statements?
- Exactly one of $x_1, x_2, x_3, x_4$ is true.
- At least two of $x_1, x_2, x_3, x_4$ are true.
- No more than two of $x_1, x_2, x_3, x_4$ are true.
logic notation first-order-logic quantifiers satisfiability
edited Dec 9 '18 at 11:30
Mauro ALLEGRANZA
67.2k449115
asked Dec 8 '18 at 20:00
Raymond HettingerRaymond Hettinger
46129
$endgroup$
add a comment |
1
$begingroup$
When working with SAT Solvers, I need to write quantifiers that give the total number of true values. The usual quantitiers $forall$ and $exists$ do not suffice. Is there a standard notation for writing the following statements?
- Exactly one of $x_1, x_2, x_3, x_4$ is true.
- At least two of $x_1, x_2, x_3, x_4$ are true.
- No more than two of $x_1, x_2, x_3, x_4$ are true.
logic notation first-order-logic quantifiers satisfiability
edited Dec 9 '18 at 11:30
Mauro ALLEGRANZA
67.2k449115
asked Dec 8 '18 at 20:00
Raymond HettingerRaymond Hettinger
46129
$endgroup$
$begingroup$
For the first you can use $exists ! _i x_i text{ is true} $. In other words $exists !$ means that there exists a unique (something) such that (something).
$endgroup$
– Yanko
Dec 8 '18 at 20:06
add a comment |
1
1
1
$begingroup$
When working with SAT Solvers, I need to write quantifiers that give the total number of true values. The usual quantitiers $forall$ and $exists$ do not suffice. Is there a standard notation for writing the following statements?
- Exactly one of $x_1, x_2, x_3, x_4$ is true.
- At least two of $x_1, x_2, x_3, x_4$ are true.
- No more than two of $x_1, x_2, x_3, x_4$ are true.
logic notation first-order-logic quantifiers satisfiability
edited Dec 9 '18 at 11:30
Mauro ALLEGRANZA
67.2k449115
asked Dec 8 '18 at 20:00
Raymond HettingerRaymond Hettinger
46129
$endgroup$
When working with SAT Solvers, I need to write quantifiers that give the total number of true values. The usual quantitiers $forall$ and $exists$ do not suffice. Is there a standard notation for writing the following statements?
- Exactly one of $x_1, x_2, x_3, x_4$ is true.
- At least two of $x_1, x_2, x_3, x_4$ are true.
- No more than two of $x_1, x_2, x_3, x_4$ are true.
logic notation first-order-logic quantifiers satisfiability
logic notation first-order-logic quantifiers satisfiability
edited Dec 9 '18 at 11:30
Mauro ALLEGRANZA
67.2k449115
asked Dec 8 '18 at 20:00
Raymond HettingerRaymond Hettinger
46129
edited Dec 9 '18 at 11:30
Mauro ALLEGRANZA
67.2k449115
asked Dec 8 '18 at 20:00
Raymond HettingerRaymond Hettinger
46129
edited Dec 9 '18 at 11:30
Mauro ALLEGRANZA
67.2k449115
edited Dec 9 '18 at 11:30
Mauro ALLEGRANZA
67.2k449115
edited Dec 9 '18 at 11:30
Mauro ALLEGRANZA
67.2k449115
67.2k449115
asked Dec 8 '18 at 20:00
Raymond HettingerRaymond Hettinger
46129
asked Dec 8 '18 at 20:00
Raymond HettingerRaymond Hettinger
46129
asked Dec 8 '18 at 20:00
Raymond HettingerRaymond Hettinger
46129
46129
$begingroup$
For the first you can use $exists ! _i x_i text{ is true} $. In other words $exists !$ means that there exists a unique (something) such that (something).
$endgroup$
– Yanko
Dec 8 '18 at 20:06
add a comment |
$begingroup$
For the first you can use $exists ! _i x_i text{ is true} $. In other words $exists !$ means that there exists a unique (something) such that (something).
$endgroup$
– Yanko
Dec 8 '18 at 20:06
$begingroup$
For the first you can use $exists ! _i x_i text{ is true} $. In other words $exists !$ means that there exists a unique (something) such that (something).
$endgroup$
– Yanko
Dec 8 '18 at 20:06
$begingroup$
For the first you can use $exists ! _i x_i text{ is true} $. In other words $exists !$ means that there exists a unique (something) such that (something).
$endgroup$
– Yanko
Dec 8 '18 at 20:06
add a comment |
1 Answer
1
active
oldest
votes
1
$begingroup$
See Generalized quantifiers :
$(∃_{=n})$ or $(∃^{=n})$ for "exactly $n$".
And :
$(∃^{ge n})$ for "at least $n$".
You can see also : Heinz-Dieter Ebbinghaus & Jörg Flum, Finite Model Theory, Springer (2nd ed., 1999), Ch.3.4 Logics with Counting Quantifiers, page 58-on.
answered Dec 8 '18 at 20:03
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
$endgroup$
$begingroup$
Is this a standard notation or something unique to the cited Stanford paper? I just did a search on "Generalized quantifers" you provided and saw a Q notation in some of the hits: ebusiness.mit.edu/research/papers/… and math.helsinki.fi/logic/opetus/ext_elem_logic/beatcs.pdf The examples included $Q_{most}$, $Q_{>=3}$, and $Q_{half}$.
$endgroup$
– Raymond Hettinger
Dec 8 '18 at 21:11
$begingroup$
@RaymondHettinger - it not very "standard" because generalized q are not often used.
$endgroup$
– Mauro ALLEGRANZA
Dec 9 '18 at 8:17
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
draft saved
draft discarded
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3031565%2fis-there-a-standard-quantifier-notation-for-an-exact-number-of-true-values%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
1
$begingroup$
See Generalized quantifiers :
$(∃_{=n})$ or $(∃^{=n})$ for "exactly $n$".
And :
$(∃^{ge n})$ for "at least $n$".
You can see also : Heinz-Dieter Ebbinghaus & Jörg Flum, Finite Model Theory, Springer (2nd ed., 1999), Ch.3.4 Logics with Counting Quantifiers, page 58-on.
answered Dec 8 '18 at 20:03
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
$endgroup$
$begingroup$
Is this a standard notation or something unique to the cited Stanford paper? I just did a search on "Generalized quantifers" you provided and saw a Q notation in some of the hits: ebusiness.mit.edu/research/papers/… and math.helsinki.fi/logic/opetus/ext_elem_logic/beatcs.pdf The examples included $Q_{most}$, $Q_{>=3}$, and $Q_{half}$.
$endgroup$
– Raymond Hettinger
Dec 8 '18 at 21:11
$begingroup$
@RaymondHettinger - it not very "standard" because generalized q are not often used.
$endgroup$
– Mauro ALLEGRANZA
Dec 9 '18 at 8:17
add a comment |
1
$begingroup$
See Generalized quantifiers :
$(∃_{=n})$ or $(∃^{=n})$ for "exactly $n$".
And :
$(∃^{ge n})$ for "at least $n$".
You can see also : Heinz-Dieter Ebbinghaus & Jörg Flum, Finite Model Theory, Springer (2nd ed., 1999), Ch.3.4 Logics with Counting Quantifiers, page 58-on.
answered Dec 8 '18 at 20:03
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
$endgroup$
$begingroup$
Is this a standard notation or something unique to the cited Stanford paper? I just did a search on "Generalized quantifers" you provided and saw a Q notation in some of the hits: ebusiness.mit.edu/research/papers/… and math.helsinki.fi/logic/opetus/ext_elem_logic/beatcs.pdf The examples included $Q_{most}$, $Q_{>=3}$, and $Q_{half}$.
$endgroup$
– Raymond Hettinger
Dec 8 '18 at 21:11
$begingroup$
@RaymondHettinger - it not very "standard" because generalized q are not often used.
$endgroup$
– Mauro ALLEGRANZA
Dec 9 '18 at 8:17
add a comment |
1
1
1
$begingroup$
See Generalized quantifiers :
$(∃_{=n})$ or $(∃^{=n})$ for "exactly $n$".
And :
$(∃^{ge n})$ for "at least $n$".
You can see also : Heinz-Dieter Ebbinghaus & Jörg Flum, Finite Model Theory, Springer (2nd ed., 1999), Ch.3.4 Logics with Counting Quantifiers, page 58-on.
answered Dec 8 '18 at 20:03
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
$endgroup$
See Generalized quantifiers :
$(∃_{=n})$ or $(∃^{=n})$ for "exactly $n$".
And :
$(∃^{ge n})$ for "at least $n$".
You can see also : Heinz-Dieter Ebbinghaus & Jörg Flum, Finite Model Theory, Springer (2nd ed., 1999), Ch.3.4 Logics with Counting Quantifiers, page 58-on.
answered Dec 8 '18 at 20:03
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
edited Dec 9 '18 at 10:57
answered Dec 8 '18 at 20:03
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
answered Dec 8 '18 at 20:03
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
answered Dec 8 '18 at 20:03
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
67.2k449115
$begingroup$
Is this a standard notation or something unique to the cited Stanford paper? I just did a search on "Generalized quantifers" you provided and saw a Q notation in some of the hits: ebusiness.mit.edu/research/papers/… and math.helsinki.fi/logic/opetus/ext_elem_logic/beatcs.pdf The examples included $Q_{most}$, $Q_{>=3}$, and $Q_{half}$.
$endgroup$
– Raymond Hettinger
Dec 8 '18 at 21:11
$begingroup$
@RaymondHettinger - it not very "standard" because generalized q are not often used.
$endgroup$
– Mauro ALLEGRANZA
Dec 9 '18 at 8:17
add a comment |
$begingroup$
Is this a standard notation or something unique to the cited Stanford paper? I just did a search on "Generalized quantifers" you provided and saw a Q notation in some of the hits: ebusiness.mit.edu/research/papers/… and math.helsinki.fi/logic/opetus/ext_elem_logic/beatcs.pdf The examples included $Q_{most}$, $Q_{>=3}$, and $Q_{half}$.
$endgroup$
– Raymond Hettinger
Dec 8 '18 at 21:11
$begingroup$
@RaymondHettinger - it not very "standard" because generalized q are not often used.
$endgroup$
– Mauro ALLEGRANZA
Dec 9 '18 at 8:17
$begingroup$
Is this a standard notation or something unique to the cited Stanford paper? I just did a search on "Generalized quantifers" you provided and saw a Q notation in some of the hits: ebusiness.mit.edu/research/papers/… and math.helsinki.fi/logic/opetus/ext_elem_logic/beatcs.pdf The examples included $Q_{most}$, $Q_{>=3}$, and $Q_{half}$.
$endgroup$
– Raymond Hettinger
Dec 8 '18 at 21:11
$begingroup$
Is this a standard notation or something unique to the cited Stanford paper? I just did a search on "Generalized quantifers" you provided and saw a Q notation in some of the hits: ebusiness.mit.edu/research/papers/… and math.helsinki.fi/logic/opetus/ext_elem_logic/beatcs.pdf The examples included $Q_{most}$, $Q_{>=3}$, and $Q_{half}$.
$endgroup$
– Raymond Hettinger
Dec 8 '18 at 21:11
$begingroup$
@RaymondHettinger - it not very "standard" because generalized q are not often used.
$endgroup$
– Mauro ALLEGRANZA
Dec 9 '18 at 8:17
$begingroup$
@RaymondHettinger - it not very "standard" because generalized q are not often used.
$endgroup$
– Mauro ALLEGRANZA
Dec 9 '18 at 8:17
add a comment |
draft saved
draft discarded
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
draft saved
draft discarded
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3031565%2fis-there-a-standard-quantifier-notation-for-an-exact-number-of-true-values%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
$begingroup$
For the first you can use $exists ! _i x_i text{ is true} $. In other words $exists !$ means that there exists a unique (something) such that (something).
$endgroup$
– Yanko
Dec 8 '18 at 20:06