## de.uni_tuebingen.sfb.lichtenstein.formulas Class SecondOrderQuantor

```java.lang.Object de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula de.uni_tuebingen.sfb.lichtenstein.formulas.SecondOrderQuantor
```
All Implemented Interfaces:
Formula, Quantification, Visitable, Serializable
Direct Known Subclasses:
SecondOrderExistentialQuantification, SecondOrderUniversalQuantification

`public abstract class SecondOrderQuantorextends ComposedFormulaimplements Quantification`

A class for representing quantors on second order variables, implementing common methods for existential and universal quantors.

Author:
Hendrik Maryns
Serialized Form

Constructor Summary
`protected ` ```SecondOrderQuantor(SecondOrderVariable var, Formula arg)```
Initialize a new quantor, given a variable to bind and a formula to act upon.

Method Summary
`protected  Set<Predicate>` `computePredicates()`
Compute the set of predicates in this formula.
`protected  Set<Variable>` `computeVariables()`
Compute the set of variables in this formula.
` boolean` `containsVariable(Variable var)`
Returns whether this formula contains the given variable.
` boolean` `equals(Object other)`
An object is equal to a quantor if it has the same class (i.e., not only it is a quantor, but it really has the same leaf-level class), the arguments are equal and they bind the same variable.
` Formula` `getArgument()`
Returns the formula this quantor acts on.
` SecondOrderVariable` `getBoundVariable()`
Returns the variable that is bound by this quantor.
` Set<Variable>` `getFreeVariables()`
Return the free variables in this formula.
` int` `getNbSubformulas()`
Returns the number of subformulas of this formula.
` Formula` `getSubformulaAt(int index)`
Returns the indexth subformula of this formula.
` int` `hashCode()`
Returns a hash code value for the object.
` boolean` `isFree(Variable variable)`
Check whether the given variable is free in this formula.
` String` `toString()`
Returns a string representation of the object.

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.ComposedFormula
`getAllSubformulas, getSymbol`

Methods inherited from class de.uni_tuebingen.sfb.lichtenstein.formulas.FormulaImpl
`and, exists, exists, forAll, forAll, getPredicates, getVariables, iff, implies, isClosed, not, or`

Methods inherited from class java.lang.Object
`clone, finalize, getClass, notify, notifyAll, wait, wait, wait`

Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Formula
`and, exists, exists, forAll, forAll, getNormalForm, getPredicates, getVariables, iff, implies, isClosed, not, or`

Methods inherited from interface de.uni_tuebingen.sfb.lichtenstein.formulas.Visitable
`accept`

Constructor Detail

### SecondOrderQuantor

```protected SecondOrderQuantor(SecondOrderVariable var,
Formula arg)```
Initialize a new quantor, given a variable to bind and a formula to act upon.

Parameters:
`var` - The variable that is bound by this quantor.
`arg` - The formula which this quantor acts upon.
Precondition:
The given variable and formula must be effective and the variable must not be bound in the given formula. | var != null && arg != null && (!arg.containsVariable(var) || arg.isFreeVariable(var))
Postconditions:
• The bound variable is set to the given variable. | new.getBoundVariable() == var
• The formula on which this quantor acts is set to the given formula. | new.getArgument() == arg
• Method Detail

### getBoundVariable

`public SecondOrderVariable getBoundVariable()`
Returns the variable that is bound by this quantor.

Specified by:
`getBoundVariable` in interface `Quantification`

### getArgument

`public Formula getArgument()`
Returns the formula this quantor acts on.

Specified by:
`getArgument` in interface `Quantification`

### computeVariables

`protected Set<Variable> computeVariables()`
Compute the set of variables in this formula. The bound variable is treated as the first variable in a quantification.

Specified by:
`computeVariables` in class `FormulaImpl`

### getFreeVariables

`public Set<Variable> getFreeVariables()`
Return the free variables in this formula. This method should be overridden for efficiency, but this class provides a correct implementation. TODO

Specified by:
`getFreeVariables` in interface `Formula`
Overrides:
`getFreeVariables` in class `FormulaImpl`
`LinkedHashSet`

### containsVariable

`public boolean containsVariable(Variable var)`
Returns whether this formula contains the given variable.

Specified by:
`containsVariable` in interface `Formula`
Parameters:
`var` - The variable to check.

### isFree

`public boolean isFree(Variable variable)`
Check whether the given variable is free in this formula.

Specified by:
`isFree` in interface `Formula`
Parameters:
`variable` - The variable to check.

### computePredicates

`protected Set<Predicate> computePredicates()`
Compute the set of predicates in this formula.

Specified by:
`computePredicates` in class `FormulaImpl`

### getNbSubformulas

`public int getNbSubformulas()`
Returns the number of subformulas of this formula.

Specified by:
`getNbSubformulas` in class `ComposedFormula`

### getSubformulaAt

```public Formula getSubformulaAt(int index)
throws IndexOutOfBoundsException```
Returns the indexth subformula of this formula.

Specified by:
`getSubformulaAt` in class `ComposedFormula`
Parameters:
`index` - The index of the wanted subformula. Indices start from 0.
Throws:
`IndexOutOfBoundsException` - `[CAN] `The index is bigger than or equal to the number of subformulas of this formula, or less than zero | index < 0 || index >= getNbSubformulas()

### equals

`public boolean equals(Object other)`
An object is equal to a quantor if it has the same class (i.e., not only it is a quantor, but it really has the same leaf-level class), the arguments are equal and they bind the same variable.

Overrides:
`equals` in class `FormulaImpl`
Returns:
If the argument of the other object, viewed as a quantor is not equal to the argument of this quantor, then false. | let otherQuantor = (Quantor) other in | if ( ! getArgument().equals(otherQuantor.getArgument()) ) | then result == false
Returns:
If the bound variable of the other object, viewed as a quantor is not equal to the bound variable of this quantor, then false. | let otherQuantor = (Quantor) other in | if ( ! getBoundVariable() == otherQuantor.getBoundVariable()) ) | then result == false

### hashCode

`public int hashCode()`
Returns a hash code value for the object.

Specified by:
`hashCode` in class `FormulaImpl`
Returns:
The hash code is based on the hash codes of the bound variable, the argument and the characteristic symbol. This last one is needed to make the difference between the various subclasses. | result == getSymbol().hashCode() + getBoundVariable().hashCode() + | getArgument().hashCode()

### toString

`public String toString()`
Returns a string representation of the object.

Specified by:
`toString` in class `FormulaImpl`
Returns:
The string representation of a quantor is the string representation of its arguments with an appropriate sign in between. | result == "(" + getSymbol() + getBoundVariable().toString() | + ")(" + getArgument().toString() + ")"

© Copyright 2008 Hendrik Maryns
{"ft_lang_label":"__label__en","ft_lang_prob":0.5146574,"math_prob":0.87446463,"size":4115,"snap":"2021-43-2021-49","text_gpt3_token_len":961,"char_repetition_ratio":0.16516663,"word_repetition_ratio":0.13976377,"special_character_ratio":0.18639125,"punctuation_ratio":0.1664,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9967083,"pos_list":[0,1,2,3,4,5,6,7,8],"im_url_duplicate_count":[null,null,null,null,null,null,null,null,null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2021-12-01T18:31:59Z\",\"WARC-Record-ID\":\"<urn:uuid:d4945837-060b-4e8f-b2a6-888823ba9c5b>\",\"Content-Length\":\"41512\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:ba8f7ad3-d9e1-48c7-b76e-ca0a6f5ee1b8>\",\"WARC-Concurrent-To\":\"<urn:uuid:d63a661f-50b4-42d2-83ab-64774bbd08eb>\",\"WARC-IP-Address\":\"134.2.5.180\",\"WARC-Target-URI\":\"http://www.tcl-sfs.uni-tuebingen.de/MonaSearch/releases/current/doc/de/uni_tuebingen/sfb/lichtenstein/formulas/SecondOrderQuantor.html\",\"WARC-Payload-Digest\":\"sha1:N4XW2QALVXKXTZZE3ABMCTP4OVQYT4Y4\",\"WARC-Block-Digest\":\"sha1:7OCFTVJLZBQU674WY6MI2JWHUFQ2EL57\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2021/CC-MAIN-2021-49/CC-MAIN-2021-49_segments_1637964360881.12_warc_CC-MAIN-20211201173718-20211201203718-00277.warc.gz\"}"}