### Install LTNtorch by cloning the repository

Source: https://github.com/logictensornetworks/ltntorch/blob/main/README.md

Alternatively, install LTNtorch by cloning the repository and installing requirements.

```bash
pip3 install -r requirements.txt
```

--------------------------------

### Visualizing the First Example of the Single Digit Dataset

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/4-semi-supervised_pattern_recognition.ipynb

This code snippet visualizes the first example from the training set of the single-digit dataset. It displays the two operand images and prints their corresponding target sum label.

```python
import matplotlib.pyplot as plt
first_example_images = single_d_train_set[0][0]
first_example_label = single_d_train_set[1][0]

print("Operands are displayed in the following images:")
fig = plt.figure()
ax = fig.add_subplot(1, 2, 1)
imgplot = plt.imshow(first_example_images[0].permute(1, 2, 0))
ax.set_title('First operand')
ax = fig.add_subplot(1, 2, 2)
imgplot = plt.imshow(first_example_images[1].permute(1, 2, 0))
ax.set_title('Second operand')
plt.show()
print("The target label (sum) for these operands is: %d" % first_example_label.item())
```

--------------------------------

### Install LTNtorch using pip

Source: https://github.com/logictensornetworks/ltntorch/blob/main/README.md

The recommended way to install LTNtorch is via pip.

```bash
pip install LTNtorch
```

--------------------------------

### Example of using \(\land\) to create a formula which is the conjunction of two predicates.

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

This example demonstrates the use of the \(\land\) operator to create a conjunction of two predicates. It highlights several key aspects of LTNtorch, including the application of connective operators to truth values, the use of Goguen conjunction, LTN broadcasting, and the structure of the resulting LTNObject.

```python
import ltn
import torch
p = ltn.Predicate(func=lambda a: torch.nn.Sigmoid()(
                                     torch.sum(a, dim=1)
                                  ))
q = ltn.Predicate(func=lambda a, b: torch.nn.Sigmoid()(
                                         torch.sum(torch.cat([a, b], dim=1),
                                     dim=1)))
x = ltn.Variable('x', torch.tensor([[0.3, 0.5],
                                     [0.04, 0.43]]))
y = ltn.Variable('y', torch.tensor([[0.5, 0.23],
                                     [4.3, 9.3],
                                     [4.3, 0.32]]))
z = ltn.Variable('z', torch.tensor([[0.3, 0.4, 0.43],
                                     [0.4, 4.3, 5.1],
                                     [1.3, 4.3, 2.3],
                                     [0.4, 0.2, 1.2]]))
And = ltn.Connective(ltn.fuzzy_ops.AndProd())
print(And)
out = And(p(x), q(y, z))
print(out)
print(out.value)
print(out.free_vars)
print(out.shape())

```

--------------------------------

### Data Preparation

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/5-regression.ipynb

Loads and preprocesses real estate data for training and testing.

```python
import torch
import pandas as pd

data = pd.read_csv("datasets/real-estate.csv")
data = data.sample(frac=1)  # shuffle

x = torch.tensor(data[['X1 transaction date', 'X2 house age',
                     'X3 distance to the nearest MRT station',
                     'X4 number of convenience stores', 'X5 latitude', 'X6 longitude']].to_numpy()).float()

y = torch.tensor(data[['Y house price of unit area']].to_numpy()).float()

x_train, y_train = x[:330], y[:330]
x_test, y_test = x[330:], y[330:]
```

--------------------------------

### Training Output

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/5-regression.ipynb

Example output from the training loop, showing epoch number, loss, training and testing satisfaction levels, and training and testing RMSE.

```text
Output:
 epoch 0 | loss 0.9997 | Train Sat 0.000 | Test Sat 0.000 | Train RMSE 189.168 | Test RMSE 178.333 
 epoch 50 | loss 0.2877 | Train Sat 0.704 | Test Sat 0.688 | Train RMSE 8.566 | Test RMSE 9.309 
 epoch 100 | loss 0.2883 | Train Sat 0.710 | Test Sat 0.689 | Train RMSE 8.817 | Test RMSE 9.262 
 epoch 150 | loss 0.2822 | Train Sat 0.718 | Test Sat 0.701 | Train RMSE 9.077 | Test RMSE 8.714 
 epoch 200 | loss 0.2715 | Train Sat 0.718 | Test Sat 0.709 | Train RMSE 8.327 | Test RMSE 8.264 
 epoch 250 | loss 0.2811 | Train Sat 0.734 | Test Sat 0.708 | Train RMSE 8.626 | Test RMSE 8.222 
 epoch 300 | loss 0.2721 | Train Sat 0.728 | Test Sat 0.727 | Train RMSE 7.677 | Test RMSE 7.802 
 epoch 350 | loss 0.2567 | Train Sat 0.736 | Test Sat 0.730 | Train RMSE 7.728 | Test RMSE 7.726 
 epoch 400 | loss 0.2558 | Train Sat 0.717 | Test Sat 0.737 | Train RMSE 7.949 | Test RMSE 7.628 
 epoch 450 | loss 0.2684 | Train Sat 0.724 | Test Sat 0.730 | Train RMSE 7.645 | Test RMSE 7.703 

```

--------------------------------

### LTN Setup and Axiom Definition

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/6-clustering.ipynb

Sets up the LTN components including the predicate, variables, constants, connectives, quantifiers, and the SatAgg operator.

```python
import ltn

# we define predicate C
class MLP(torch.nn.Module):
    """
    Here, the problem of clustering is organized as a classification task, where the classifier outputs the probability
    that the point given in input belongs to a specific cluster. The clusters are the classes of the classification
    problem.
    """
    def __init__(self, layer_sizes=(2, 16, 16, 16, 4)):
        super(MLP, self).__init__()
        self.elu = torch.nn.ELU()
        self.softmax = torch.nn.Softmax(dim=1)
        self.linear_layers = torch.nn.ModuleList([torch.nn.Linear(layer_sizes[i - 1], layer_sizes[i])
                                                  for i in range(1, len(layer_sizes))])

    def forward(self, x, c):
        """
        Given a point x and a cluster c, the forward phase of this MLP returns the probability that the point x belongs
        to cluster c.

        :param x: point that has to be assigned to a cluster
        :param c: cluster for which we want to compute the probability
        :return: the probability that point x belong to cluster c
        """
        for layer in self.linear_layers[:-1]:
            x = self.elu(layer(x))
        x = self.softmax(self.linear_layers[-1](x))
        out = torch.sum(x * c, dim=1)
        return out

C = ltn.Predicate(MLP())

# we define the variables
c = ltn.Variable("c", torch.tensor([[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 1, 0], [0, 0, 0, 1]]))
x = ltn.Variable("x", torch.tensor(data))
y = ltn.Variable("y", torch.tensor(data))

# we define the constants
th_close = ltn.Constant(torch.tensor(close_threshold))
th_distant = ltn.Constant(torch.tensor(distant_threshold))

# we define connectives, quantifiers, and the SatAgg operator
And = ltn.Connective(ltn.fuzzy_ops.AndProd())
Not = ltn.Connective(ltn.fuzzy_ops.NotStandard())
Equiv = ltn.Connective(ltn.fuzzy_ops.Equiv(ltn.fuzzy_ops.AndProd(), ltn.fuzzy_ops.ImpliesReichenbach()))
Exists = ltn.Quantifier(ltn.fuzzy_ops.AggregPMean(p=1), quantifier="e")
Forall = ltn.Quantifier(ltn.fuzzy_ops.AggregPMeanError(p=4), quantifier="f")
SatAgg = ltn.fuzzy_ops.SatAgg()

```

--------------------------------

### Trainable constant

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

Example of creating and using a trainable LTN constant.

```python
t_c = ltn.Constant(torch.tensor([[3.4, 2.3, 5.6],
                                 [6.7, 5.6, 4.3]]), trainable=True)
print(t_c)
print(t_c.value)
print(t_c.free_vars)
print(t_c.shape())
```

--------------------------------

### Diagonal Quantification Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

Demonstrates the usage of diagonal quantification in Logic Tensor Networks compared to standard quantification.

```python
>>> x = ltn.Variable('x', torch.tensor([[0.3, 1.3],
                                      [0.3, 0.3]]))
>>> y = ltn.Variable('y', torch.tensor([[2.3, 0.3],
                                     [1.2, 3.4]]))
```

```python
>>> out = Forall(ltn.diag(x, y), p(x, y)) # with diagonal quantification
>>> out_without_diag = Forall([x, y], p(x, y)) # without diagonal quantification
```

```python
>>> print(out_without_diag)
LTNObject(value=tensor(0.9788), free_vars=[])
>>> print(out_without_diag.value)
tensor(0.9788)
```

```python
>>> print(out)
LTNObject(value=tensor(0.9888), free_vars=[])
>>> print(out.value)
tensor(0.9888)
```

```python
>>> print(out.free_vars)
[]
```

```python
>>> print(out.shape())
torch.Size([])
```

--------------------------------

### Data Loaders

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/5-regression.ipynb

Creates PyTorch DataLoader instances for training and testing datasets.

```python
train_loader = DataLoader(x_train, y_train, 64, shuffle=True)
test_loader = DataLoader(x_test, y_test, 64, shuffle=False)
```

--------------------------------

### Stable pMean Operator Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/tutorials/2b-operators-and-gradients.ipynb

Demonstrates the use of the stable version of the pMean operator to solve exploding gradient problems.

```python
xs = torch.tensor([1., 1., 1.], requires_grad=True)

# the exploding gradient problem is solved
y = forall_pME(xs, dim=0, p=4, stable=True)
res = y.item()
y.backward()
gradients = xs.grad
# print the result of the aggregation
print(res)
# print the gradients of xs
print(gradients)
```

--------------------------------

### Diagonal Quantification Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/quantification.html

Illustrates how diagonal quantification works by comparing it to standard quantification and showing the expected output tensor shape.

```python
forall Diag(x, y) P(x, y)
```

--------------------------------

### Diagonal Quantification Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

Demonstrates the use of `ltn.diag()` for diagonal quantification, showing the resulting value, free variables, and shape.

```python
import ltn
import torch
p = ltn.Predicate(func=lambda a, b: torch.nn.Sigmoid()(
                                        torch.sum(torch.cat([a, b], dim=1), dim=1)
                                    ))
x = ltn.Variable('x', torch.tensor([[0.3, 0.56, 0.43], [0.3, 0.5, 0.04]]))
y = ltn.Variable('y', torch.tensor([[0.4, 0.004], [0.3, 0.32]]))
x, y = ltn.diag(x, y)
out = p(x, y)
print(out.value)
print(out.free_vars)
print(out.shape())
```

--------------------------------

### AggregMean Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/fuzzy_ops.html

Illustrates the use of the AggregMean operator for fuzzy aggregation, showing quantifier creation and application with a predicate.

```python
import ltn
import torch
Forall = ltn.Quantifier(ltn.fuzzy_ops.AggregMean(), quantifier='f')
print(Forall)
p = ltn.Predicate(func=lambda x: torch.nn.Sigmoid()(
                                     torch.sum(x, dim=1)
                                  ))
x = ltn.Variable('x', torch.tensor([[0.56], [0.9], [0.7]]))
print(p(x).value)
print(Forall(x, p(x)).value)
```

--------------------------------

### Binary function defined using a function

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

This example demonstrates defining a binary function using a lambda function, showcasing input concatenation and aggregation.

```python
b_f_f = ltn.Function(func=lambda x, y:
                                 torch.repeat_interleave(
                                     torch.sum(torch.cat([x, y], dim=1), dim=1, keepdim=True), 2,
                                     dim=1))
print(b_f_f)
```

--------------------------------

### Undiagonalization Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

Demonstrates the use of `ltn.undiag()` to restore LTN broadcasting after diagonal quantification, showing the resulting value, free variables, and shape.

```python
x, y = ltn.undiag(x, y)
out = p(x, y)
print(out.value)
print(out.free_vars)
print(out.shape())
```

--------------------------------

### Import necessary libraries

Source: https://github.com/logictensornetworks/ltntorch/blob/main/tutorials/3-knowledgebase-and-learning.ipynb

Imports the required libraries for the tutorial: torch, numpy, ltn, and matplotlib.

```python
import torch
import numpy as np
import ltn
import matplotlib.pyplot as plt
```

--------------------------------

### Multi-digit Training and Testing Loop

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/4-semi-supervised_pattern_recognition.ipynb

This code snippet shows the training and testing loop for the multi-digit case. It includes optimizer setup, parameter scheduling, and the core logic for grounding variables, defining logical formulas, calculating loss, and computing accuracy.

```python
optimizer = torch.optim.Adam(Digit_m_d.parameters(), lr=0.001)

for epoch in range(20):
    # scheduling of the parameter p for the existential quantifier as described in the LTN paper
    if epoch in range(0, 4):
        p = 1
    if epoch in range(4, 8):
        p = 2
    if epoch in range(8, 12):
        p = 4
    if epoch in range(12, 20):
        p = 6
    train_loss, test_loss = 0.0, 0.0
    train_sat, test_sat = 0.0, 0.0
    train_acc, test_acc = 0.0, 0.0
    # train step
    for batch_idx, (operand_images, addition_label) in enumerate(multi_d_train_loader):
        optimizer.zero_grad()
        # ground variables with current batch data
        images_x1 = ltn.Variable("x1", operand_images[:, 0])
        images_x2 = ltn.Variable("x2", operand_images[:, 1])
        images_y1 = ltn.Variable("y1", operand_images[:, 2])
        images_y2 = ltn.Variable("y2", operand_images[:, 3])
        labels_z = ltn.Variable("z", addition_label)
        sat_agg = Forall(
            ltn.diag(images_x1, images_x2, images_y1, images_y2, labels_z),
            Exists(
                [d_1, d_2, d_3, d_4],
                And(
                    And(Digit_m_d(images_x1, d_1),Digit_m_d(images_x2, d_2)),
                    And(Digit_m_d(images_y1, d_3),Digit_m_d(images_y2, d_4))
                ),
                cond_vars=[d_1, d_2, d_3, d_4, labels_z],
                cond_fn=lambda d1, d2, d3, d4, z: torch.eq(10 * d1.value + d2.value + 10 * d3.value + d4.value, z.value),
                p=p
            )).value
        loss = 1. - sat_agg
        loss.backward()
        optimizer.step()
        train_loss += loss.item()
        train_sat += sat_agg
        # compute train accuracy
        predictions_x1 = torch.argmax(cnn_m_d(operand_images[:, 0].to(ltn.device)), dim=1)
        predictions_x2 = torch.argmax(cnn_m_d(operand_images[:, 1].to(ltn.device)), dim=1)
        predictions_y1 = torch.argmax(cnn_m_d(operand_images[:, 2].to(ltn.device)), dim=1)
        predictions_y2 = torch.argmax(cnn_m_d(operand_images[:, 3].to(ltn.device)), dim=1)
        predictions = 10 * predictions_x1 + predictions_x2 + 10 * predictions_y1 + predictions_y2
        train_acc += torch.count_nonzero(torch.eq(addition_label.to(ltn.device), predictions)) / predictions.shape[0]
    train_loss = train_loss / len(multi_d_train_loader)
    train_sat = train_sat / len(multi_d_train_loader)
    train_acc = train_acc / len(multi_d_train_loader)

    # test step
    for batch_idx, (operand_images, addition_label) in enumerate(multi_d_test_loader):
        # ground variables with current batch data
        images_x1 = ltn.Variable("x1", operand_images[:, 0])
        images_x2 = ltn.Variable("x2", operand_images[:, 1])
        images_y1 = ltn.Variable("y1", operand_images[:, 2])
        images_y2 = ltn.Variable("y2", operand_images[:, 3])
        labels_z = ltn.Variable("z", addition_label)
        sat_agg = Forall(
            ltn.diag(images_x1, images_x2, images_y1, images_y2, labels_z),
            Exists(
                [d_1, d_2, d_3, d_4],
                And(
                    And(Digit_m_d(images_x1, d_1),Digit_m_d(images_x2, d_2)),
                    And(Digit_m_d(images_y1, d_3),Digit_m_d(images_y2, d_4))
                ),
                cond_vars=[d_1, d_2, d_3, d_4, labels_z],
                cond_fn=lambda d1, d2, d3, d4, z: torch.eq(10 * d1.value + d2.value + 10 * d3.value + d4.value, z.value),
                p=p
            )).value
        loss = 1. - sat_agg
        test_loss += loss.item()
        test_sat += sat_agg
        # compute test accuracy
        predictions_x1 = torch.argmax(cnn_m_d(operand_images[:, 0].to(ltn.device)), dim=1)
        predictions_x2 = torch.argmax(cnn_m_d(operand_images[:, 1].to(ltn.device)), dim=1)
        predictions_y1 = torch.argmax(cnn_m_d(operand_images[:, 2].to(ltn.device)), dim=1)
        predictions_y2 = torch.argmax(cnn_m_d(operand_images[:, 3].to(ltn.device)), dim=1)
        predictions = 10 * predictions_x1 + predictions_x2 + 10 * predictions_y1 + predictions_y2
        test_acc += torch.count_nonzero(torch.eq(addition_label.to(ltn.device), predictions)) / predictions.shape[0]
    test_loss = test_loss / len(multi_d_test_loader)
    test_sat = test_sat / len(multi_d_test_loader)
    test_acc = test_acc / len(multi_d_test_loader)

    # we print metrics every epoch of training

    print(" epoch %d | Train loss %.4f | Train Sat %.4f | Train Acc %.4f | Test loss %.4f | Test Sat %.4f |" \
                " Test Acc %.4f " %
          (epoch, train_loss, train_sat, train_acc, test_loss, test_sat, test_acc))
```

--------------------------------

### Defining Variables and Constants

Source: https://github.com/logictensornetworks/ltntorch/blob/main/tutorials/3-knowledgebase-and-learning.ipynb

This snippet shows how to define variables and constants using LTN, including tensors for points and weights.

```python
x1 = ltn.Variable("x1", torch.tensor(points))
x2 = ltn.Variable("x2", torch.tensor(points))
a = ltn.Constant(torch.tensor([3.3, 2.5]))
b = ltn.Constant(torch.tensor([1.3, 1.1]))
l_a = ltn.Constant(torch.tensor([1, 0]))
l_b = ltn.Constant(torch.tensor([0, 1]))
l = ltn.Variable("l", torch.tensor([[1, 0], [0, 1]]))

```

--------------------------------

### Dataset generation and plotting

Source: https://github.com/logictensornetworks/ltntorch/blob/main/tutorials/3-knowledgebase-and-learning.ipynb

This code generates a dataset of 10000 points and plots them, highlighting specific points 'a' and 'b'.

```python
r1 = 0
r2 = 4
points = (r1 - r2) * torch.rand((10000, 2)) + r2
points[-1] = torch.tensor([3., 3.])
points[-2] = torch.tensor([1., 1.])
points_a = torch.tensor([3., 3.])
points_b = torch.tensor([1., 1.])
a = ltn.Constant(torch.tensor([3., 3.]))
b = ltn.Constant(torch.tensor([1., 1.]))

fig, ax = plt.subplots()
ax.set_xlim(0, 4)
ax.set_ylim(0, 4)
ax.scatter(points[:,0], points[:,1], color="black", label="unknown")
ax.scatter(point_a[0], point_a[1], color="blue", label="a")
ax.scatter(point_b[0], point_b[1], color="red", label="b")
ax.set_title("Dataset of individuals")
plt.legend()
```

--------------------------------

### Pseudo-code for standard vs. diagonal quantification

Source: https://github.com/logictensornetworks/ltntorch/blob/main/tutorials/2-grounding_connectives.ipynb

Illustrates the difference in iteration logic between standard quantification (broadcasting) and diagonal quantification (zipping).

```python
for x_i in x:
    for y_j in y:
        results.append(P(x_i,y_j))
aggregate(results)
```

```python
for x_i, y_i in zip(x,y):
    results.append(P(x_i,y_i))
aggregate(results)
```

--------------------------------

### Non-trainable constant

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

Example of creating and using a non-trainable LTN constant.

```python
import ltn
import torch
c = ltn.Constant(torch.tensor([3.4, 5.4, 4.3]))
print(c)
print(c.value)
print(c.free_vars)
print(c.shape())
```

--------------------------------

### Utility Classes and Functions

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/5-regression.ipynb

Defines a PyTorch DataLoader and functions to evaluate model performance (satisfaction level and RMSE).

```python
import numpy as np
from sklearn.metrics import mean_squared_error

# this is a standard PyTorch DataLoader to load the dataset for the training and testing of the model
class DataLoader(object):
    def __init__(self,
                 x,
                 y,
                 batch_size=1,
                 shuffle=True):
        self.x = x
        self.y = y
        self.batch_size = batch_size
        self.shuffle = shuffle

    def __len__(self):
        return int(np.ceil(self.x.shape[0] / self.batch_size))

    def __iter__(self):
        n = self.x.shape[0]
        idxlist = list(range(n))
        if self.shuffle:
            np.random.shuffle(idxlist)

        for _, start_idx in enumerate(range(0, n, self.batch_size)):
            end_idx = min(start_idx + self.batch_size, n)
            x = self.x[idxlist[start_idx:end_idx]]
            y = self.y[idxlist[start_idx:end_idx]]

            yield x, y

# define metrics for evaluation of the model

# it computes the overall satisfaction level on the knowledge base using the given data loader (train or test)
def compute_sat_level(loader):
    mean_sat = 0
    for x_data, y_data in loader:
        x = ltn.Variable("x", x_data)
        y = ltn.Variable("y", y_data)
        mean_sat += Forall(ltn.diag(x, y), Eq(f(x), y)).value
    mean_sat /= len(loader)
    return mean_sat

# it computes the overall RMSE between the predictions and the ground truth, using the given data loader (train or test)
def compute_rmse(loader):
    mean_rmse = 0.0
    for x, y in loader:
        predictions = f.model(x).detach().numpy()
        mean_rmse += mean_squared_error(y, predictions, squared=False)
    return mean_rmse / len(loader)
```

--------------------------------

### Variable with add_batch_dim=True

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

Example of creating an LTN variable where add_batch_dim=True has no effect because the value already has a batch dimension.

```python
import ltn
import torch
x = ltn.Variable('x', torch.tensor([[3.4, 4.5],
                                     [6.7, 9.6]]), add_batch_dim=True)
print(x)
print(x.value)
print(x.free_vars)
print(x.shape())
```

--------------------------------

### Godel Implication Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/fuzzy_ops.html

Demonstrates the use of the Godel fuzzy implication operator with LTN variables and predicates.

```python
import ltn
import torch
Implies = ltn.Connective(ltn.fuzzy_ops.ImpliesGodel())
print(Implies)
p = ltn.Predicate(func=lambda x: torch.nn.Sigmoid()(
                                     torch.sum(x, dim=1)
                                  ))
x = ltn.Variable('x', torch.tensor([[0.56], [0.9]]))
y = ltn.Variable('y', torch.tensor([[0.7], [0.2], [0.1]]))
print(p(x).value)
print(p(y).value)
print(Implies(p(x), p(y)).value)
```

--------------------------------

### LTN Setup: Predicates, Connectives, and Quantifiers

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/7-learning_embeddings_with_LTN.ipynb

Defines the LTN predicates (C, S, F) using MLP models and sets up the fuzzy logic connectives (And, Not, Implies), quantifiers (Exists, Forall), and the SatAgg operator.

```python
# we define predicates F, C, and S
class MLP(torch.nn.Module):
    """
    Simple MLP model used for defining the predicates of our problem.
    """
    def __init__(self, layer_sizes=(10, 16, 16, 1)):
        super(MLP, self).__init__()
        self.elu = torch.nn.ELU()
        self.sigmoid = torch.nn.Sigmoid()
        self.linear_layers = torch.nn.ModuleList([torch.nn.Linear(layer_sizes[i - 1], layer_sizes[i])
                                                  for i in range(1, len(layer_sizes))])

    def forward(self, *x):
        """
        Given an individual x, the forward phase of this MLP returns the probability that the individual x is a smoker,
        or has cancer, or is friend of y (if given and predicate is F).

        :param x: individuals for which we have to compute the probability
        :return: the probability that individual x is a smoker, or has cancer, or is friend of y (if given)
        """
        x = list(x)
        if len(x) == 1:
            x = x[0]
        else:
            x = torch.cat(x, dim=1)
        for layer in self.linear_layers[:-1]:
            x = self.elu(layer(x))
        out = self.sigmoid(self.linear_layers[-1](x))
        return out

C = ltn.Predicate(MLP(layer_sizes=(5, 16, 16, 1)))
S = ltn.Predicate(MLP(layer_sizes=(5, 16, 16, 1)))
F = ltn.Predicate(MLP(layer_sizes=(10, 16, 16, 1)))

# we define connectives, quantifiers, and SatAgg
And = ltn.Connective(ltn.fuzzy_ops.AndProd())
Not = ltn.Connective(ltn.fuzzy_ops.NotStandard())
Implies = ltn.Connective(ltn.fuzzy_ops.ImpliesReichenbach())
Exists = ltn.Quantifier(ltn.fuzzy_ops.AggregPMean(p=2), quantifier="e")
Forall = ltn.Quantifier(ltn.fuzzy_ops.AggregPMeanError(p=2), quantifier="f")
SatAgg = ltn.fuzzy_ops.SatAgg()
```

--------------------------------

### Kleene-Dienes Implication Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/fuzzy_ops.html

Demonstrates the use of the Kleene-Dienes fuzzy implication operator with LTN variables and predicates.

```python
import ltn
import torch
Implies = ltn.Connective(ltn.fuzzy_ops.ImpliesKleeneDienes())
print(Implies)
p = ltn.Predicate(func=lambda x: torch.nn.Sigmoid()(
                                     torch.sum(x, dim=1)
                                  ))
x = ltn.Variable('x', torch.tensor([[0.56], [0.9]]))
y = ltn.Variable('y', torch.tensor([[0.7], [0.2], [0.1]]))
print(p(x).value)
print(p(y).value)
print(Implies(p(x), p(y)).value)
```

--------------------------------

### Setting up variables and a classifier model for diagonal quantification

Source: https://github.com/logictensornetworks/ltntorch/blob/main/tutorials/2-grounding_connectives.ipynb

Defines random samples and labels, creates LTN variables, and initializes a PyTorch model for classification.

```python
# The values are generated at random, for the sake of illustration.
# In a real scenario, they would come from a dataset.
samples = torch.randn((100, 2, 2)) # 100 R^{2x2} values
labels = torch.randint(0, 3, size=(100,)) # 100 labels (class 0/1/2) that correspond to each sample
onehot_labels = torch.nn.functional.one_hot(labels, num_classes=3)

x = ltn.Variable("x", samples)
l = ltn.Variable("l", onehot_labels)

class ModelC(torch.nn.Module):
    def __init__(self):
        super(ModelC, self).__init__()
        self.elu = torch.nn.ELU()
        self.softmax = torch.nn.Softmax(dim=1)
        self.dense1 = torch.nn.Linear(4, 5)
        self.dense2 = torch.nn.Linear(5, 3)

    def forward(self, x, l):
        x = torch.flatten(x, start_dim=1)
        x = self.elu(self.dense1(x))
        x = self.softmax(self.dense2(x))
        return torch.sum(x * l, dim=1)

C = ltn.Predicate(ModelC())
```

--------------------------------

### Unary predicate defined using a torch.nn.Sequential

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/core.html

Example of defining an LTN predicate using a PyTorch Sequential model.

```python
>>> import ltn
>>> import torch
>>> predicate_model = torch.nn.Sequential(
...                         torch.nn.Linear(4, 2),
...                         torch.nn.ELU(),
...                         torch.nn.Linear(2, 1),
...                         torch.nn.Sigmoid()
...                   )
>>> p = ltn.Predicate(model=predicate_model)
>>> print(p)
Predicate(model=Sequential(
  (0): Linear(in_features=4, out_features=2, bias=True)
  (1): ELU(alpha=1.0)
  (2): Linear(in_features=2, out_features=1, bias=True)
  (3): Sigmoid()
))
```

--------------------------------

### LTN Setup: Constants, Predicates, and Operators

Source: https://github.com/logictensornetworks/ltntorch/blob/main/examples/3-multi_class_multi_label_classification.ipynb

Defines the LTN constants for labels (blue, orange, male, female), sets up the predicate P using an MLP for logits and a wrapper to convert logits to probabilities for a specific class, and initializes LTN connectives, quantifiers, and the SatAgg operator.

```python
import ltn

# we define the constants
l_blue = ltn.Constant(torch.tensor([1, 0, 0, 0]))
l_orange = ltn.Constant(torch.tensor([0, 1, 0, 0]))
l_male = ltn.Constant(torch.tensor([0, 0, 1, 0]))
l_female = ltn.Constant(torch.tensor([0, 0, 0, 1]))

# we define predicate P
class MLP(torch.nn.Module):
    """
    This model returns the logits for the classes given an input example. It does not compute the softmax, so the output
    are not normalized.
    This is done to separate the accuracy computation from the satisfaction level computation. Go through the example
    to understand it.
    """
    def __init__(self, layer_sizes=(5, 16, 16, 8, 4)):
        super(MLP, self).__init__()
        self.elu = torch.nn.ELU()
        self.dropout = torch.nn.Dropout(0.2)
        self.linear_layers = torch.nn.ModuleList([torch.nn.Linear(layer_sizes[i - 1], layer_sizes[i])
                                                  for i in range(1, len(layer_sizes))])

    def forward(self, x, training=False):
        """
        Method which defines the forward phase of the neural network for our multi class classification task.
        In particular, it returns the logits for the classes given an input example.

        :param x: the features of the example
        :param training: whether the network is in training mode (dropout applied) or validation mode (dropout not applied)
        :return: logits for example x
        """
        for layer in self.linear_layers[:-1]:
            x = self.elu(layer(x))
            if training:
                x = self.dropout(x)
        logits = self.linear_layers[-1](x)
        return logits


class LogitsToPredicate(torch.nn.Module):
    """
    This model has inside a logits model, that is a model which compute logits for the classes given an input example x.
    The idea of this model is to keep logits and probabilities separated. The logits model returns the logits for an example, 
    while this model returns the probabilities given the logits model.

    In particular, it takes as input an example x and a class label l. It applies the logits model to x to get the logits.
    Then, it applies a softmax function to get the probabilities per classes. Finally, it returns only the probability related
    to the given class l.
    """
    def __init__(self, logits_model):
        super(LogitsToPredicate, self).__init__()
        self.logits_model = logits_model
        self.sigmoid = torch.nn.Sigmoid()

    def forward(self, x, l, training=False):
        logits = self.logits_model(x, training=training)
        probs = self.sigmoid(logits)
        out = torch.sum(probs * l, dim=1)
        return out

mlp = MLP()
P = ltn.Predicate(LogitsToPredicate(mlp))

# we define the connectives, quantifiers, and the SatAgg
Not = ltn.Connective(ltn.fuzzy_ops.NotStandard())
And = ltn.Connective(ltn.fuzzy_ops.AndProd())
Forall = ltn.Quantifier(ltn.fuzzy_ops.AggregPMeanError(p=2), quantifier="f")
SatAgg = ltn.fuzzy_ops.SatAgg()

```

--------------------------------

### pMean fuzzy aggregation operator

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/fuzzy_ops.html

Example demonstrating the usage of the pMean fuzzy aggregation operator with a Quantifier and a Predicate.

```python
import ltn
import torch
Exists = ltn.Quantifier(ltn.fuzzy_ops.AggregPMean(), quantifier='e')
print(Exists)
p = ltn.Predicate(func=lambda x: torch.nn.Sigmoid()(
                                     torch.sum(x, dim=1)
                                  ))
x = ltn.Variable('x', torch.tensor([[0.56], [0.9], [0.7]]))
print(p(x).value)
print(Exists(x, p(x)).value)
```

--------------------------------

### AggregMin Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/fuzzy_ops.html

Demonstrates the usage of the AggregMin operator for fuzzy aggregation, including creating a quantifier and applying it to a predicate.

```python
import ltn
import torch
Forall = ltn.Quantifier(ltn.fuzzy_ops.AggregMin(), quantifier='f')
print(Forall)
p = ltn.Predicate(func=lambda x: torch.nn.Sigmoid()(
                                     torch.sum(x, dim=1)
                                  ))
x = ltn.Variable('x', torch.tensor([[0.56], [0.9], [0.7]]))
print(p(x).value)
print(Forall(x, p(x)).value)
```

--------------------------------

### Standard Fuzzy Negation (NotStandard)

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/fuzzy_ops.html

This example demonstrates the usage of the standard fuzzy negation operator. It shows how to instantiate the operator, apply it to a predicate's output, and observe the resulting negated values.

```python
import ltn
import torch
Not = ltn.Connective(ltn.fuzzy_ops.NotStandard())
print(Not)
p = ltn.Predicate(func=lambda x: torch.nn.Sigmoid()(
                                    torch.sum(x, dim=1)
                                 ))
x = ltn.Variable('x', torch.tensor([[0.56], [0.9]]))
print(p(x).value)
print(Not(p(x)).value)
```

--------------------------------

### Equiv Operator Example

Source: https://github.com/logictensornetworks/ltntorch/blob/main/docs/fuzzy_ops.html

Demonstrates the usage of the Equiv fuzzy operator with AndProd and ImpliesReichenbach, showing broadcasting behavior.

```python
import ltn
import torch
Equiv = ltn.Connective(ltn.fuzzy_ops.Equiv(
                            and_op=ltn.fuzzy_ops.AndProd(),
                            implies_op=ltn.fuzzy_ops.ImpliesReichenbach()
                        ))
print(Equiv)
p = ltn.Predicate(func=lambda x: torch.nn.Sigmoid()(
                                    torch.sum(x, dim=1)
                                 ))
x = ltn.Variable('x', torch.tensor([[0.56], [0.9]]))
y = ltn.Variable('y', torch.tensor([[0.7], [0.2], [0.1]]))
print(p(x).value)
print(p(y).value)
print(Equiv(p(x), p(y)).value)
```

--------------------------------

### Training a predicate C

Source: https://github.com/logictensornetworks/ltntorch/blob/main/tutorials/3-knowledgebase-and-learning.ipynb

This code snippet shows the process of training a predicate 'C' using an Adam optimizer to minimize a loss function derived from a knowledge base.

```python
optimizer = torch.optim.Adam(C.parameters(), lr=0.001)

for epoch in range(2000):
    optimizer.zero_grad()
    loss = 1. - sat_agg(
        C(a, l_a), 
        C(b, l_b),
        Forall([x1, x2, l], Implies(Sim(x1, x2), Equiv(C(x1, l), C(x2, l))))
    )
    loss.backward()
    optimizer.step()
    if epoch%200 == 0:
        print("Epoch %d: Sat Level %.3f "%(epoch, 1 - loss.item()))
print("Training finished at Epoch %d with Sat Level %.3f" %(epoch, 1 - loss.item()))
```