Since half past the last century, the Cloze test has been used for educational purposes to assess proficiency in understanding texts in different languages Taylor [1953], Brown [1980, 2002]. The task consists of the systematic filling in of gaps in a text, specifically a prose selection Bickley et al. [1970], previously adapted to the participant's realities, and the scores of correct answers are associated with the degree of comprehension of the text by the participant. Different measures, such as exact answer, acceptable answer Brown [1980], multiple choice, and Clozentropy Darnell [1968], Lowry and Marr [1975], have been used to assess gap-filling since Taylor's initial proposal Taylor [1953]. These measures will be further examined in Section 2. The exact answer may seem easier to calculate, especially for a Cloze test applied to large and heterogeneous groups of students with insufficient time for teachers to analyze each answer individually. In Brazil, for instance, teachers usually have to manage numerous classes, and this correction method helps to provide rapid answers to students' reading proficiency, allowing one to check the answers objectively Cunha and Santos [2010] without possible or different options.

Many existing boundedly-suboptimal heuristic search algorithms are variants of best-first search. Due to memory limitations, these algorithms are unable to solve problems with extremely large search spaces. In this paper, we present a framework that allows best-first search algorithms to solve problems with such large search spaces given a (reasonable) memory bound while also preserving optimality guarantees in tree-structured search spaces. In our framework, a given algorithm is run several times. In each search episode, the algorithm expands up to a user-defined number of states. After each episode, unless the goal has been found, the heuristic values of the generated states are updated using a linear-time algorithm that preserves consistency in tree-structured search spaces. In subsequent search episodes, only the heuristic values of the states generated in the previous episode need to be kept in memory. We present experimental results where we plug A*, GBFS, and wA* into our framework to solve traveling salesman problems and compare them against benchmark linear-memory algorithms like DFBnB and wDFBnB.

Logic is the science of correct inferences and a logical system is a tool to prove assertions in a certain logic in a correct way. There are many logical systems, and many ways of formalizing them, e.g., using natural deduction or sequent calculus. Calculus of structures (CoS) is a new formalism proposed by Alessio Guglielmi in 2004 that generalizes sequent calculus in the sense that inference rules can be applied at any depth inside a formula, rather than only to the main connective. With this feature, proofs in CoS are shorter than in any other formalism supporting analytical proofs. Although it is great to have the freedom and expressiveness of CoS, under the point of view of proof search more freedom means a larger search space. And that should be restricted when looking for complete automation of deductive systems. Some efforts were made to reduce this non-determinism, but they are all basically operational approaches, and no solid theoretical result regarding the computational behaviour of CoS has been achieved so far. The main focus of this thesis is to discuss ways to propose a proof search strategy for CoS suitable to implementation. This strategy should be theoretical instead of purely operational. We introduce the concept of incoherence number of substructures inside structures and we use this concept to achieve our main result: there is an algorithm that, according to our conjecture, corresponds to a proof search strategy to every provable structure in the subsystem of FBV (the multiplicative linear logic MLL plus the rule mix) containing only pairwise distinct atoms. Our algorithm is implemented and we believe our strategy is a good starting point to exploit the computational aspects of CoS in more general systems, like BV itself.