In this dissertation we investigate theoretical aspects of some practical approaches used in solving and understanding search problems. We concentrate on the Satisfiability problem, which is a strong representative from search problem domains. The work develops general theoretical foundations to investigate some practical aspects of satisfiability search. This results in a better understanding of the fundamental mechanics for search algorithm construction and behaviour. A theory of choice or branching heuristics is presented, accompanied by results showing a correspondence of both parameterisations and performance when the method is compared to previous empirically motivated branching techniques. The logical foundations of the backtracking mechanism are explored alongside formulations for reasoning in relevant logics which results in the development of a malleable backtracking mechanism that subsumes other intelligent backtracking proof construction techniques and allows the incorporation of proof rearrangement strategies. Moreover, empirical tests show that relevant backtracking outperforms all other forms of intelligent backtracking search tree construction methods. An investigation into modelling and generating world problem instances justifies a modularised problem model proposal which is used experimentally to highlight the practicability of search algorithms for the proposed model and related domains.

[pt] O objetivo desta dissertação é construir um tableaux linear intuicionista a partir de um cálculo de sequentes relevante clássico. Os passos principais dessa construção são: i) tradução das regras do cálculo dos sequentes relevante clássico para regras de tableaux (capítulo 3), usando a estratégia apresentada por D Agostino et al. em Tableau Methods for Substructural Logic. ii) construção de um tableaux linear clássico através da linearização do tableaux clássico relevante (capítulo 4). iii) apresentar um tableau intuicionista ao estilo Fitting, em que são adicionados rótulos T s e F s às fórmulas (capítulo 5). / [en] The main goal of this master tesis is intuitionistic linear tableaux from a relevant sequent calculus. The central steps are: i) Apply D Agostino et al. strategy to translate classical relevant sequent calculus rules to tableaux rules for classical relevant logic (Chapter 3). ii) Use Meyer et al. strategy to linearize the classical relevant tableaux (Chapter 4). iii) Build a new intuicionistic linear tableaux with Fitting labels.