1,721,082 research outputs found
A note on the analysis of theorem-proving strategies
Full text linkThis paper presents the main tenets of an approach to the analysis of the search complexity of theorem proving strategies, showing how to capture formally the effects of contraction inference rules on the search space
Problems in Lukasiewicz logic
No full textIn the November 1990 issue of this Newsletter, Larry Wos described a problem in Lukasiewicz logic as a challenge problem for theorem provers. This note is intended to provide additional information to anyone interested in attacking the problem with an automated prover. We present three problems in Lukasiewicz logic and the results obtained so far in proving them automatically
Sulla dimostrazione di teoremi per completamento
No full textQuesta tesi è uno studio delle procedure di completamento di tipo Knuth-Bendix per dimostrazione di teoremi, generazione di procedure di decisione, dimostrazione di teoremi induttivi e programmazione logica. La tesi offre una nuova presentazione delle procedure di completamento, dove il concetto di base è la riduzione di prove
A taxonomy of parallel strategies for deduction
Full text linkThis paper presents a taxonomy of parallel theorem-proving methods based on the control of search (e.g., master-slaves versus peer processes), the granularity of parallelism (e.g., fine, medium and coarse grain) and the nature of the method (e.g., ordering-based versus subgoal-reduction). We analyze how the different approaches to parallelization affect the control of search: while fine and medium-grain methods, as well as master-slaves methods, generally do not modify the sequential search plan, parallel-search methods may combine sequential search plans (multi-search) or extend the search plan with the capability of subdividing the search space (distributed search). Precisely because the search plan is modified, the latter methods may produce radically different searches than their sequential base, as exemplified by the first distributed proof of the Robbins theorem generated by the Modified Clause-Diffusion prover Peers-mcd. An overview of the state of the field and directions for future research conclude the paper
A model and a first analysis of distributed-search contraction-based strategies
Full text linkWhile various approaches to parallel theorem proving have been proposed, their usefulness is evaluated only empirically. This research is a contribution towards the goal of machine-independent analysis of theorem-proving strategies. This paper considers clausal contraction-based strategies and their parallelization by distributed search, with subdivision of the search space and propagation of clauses by message-passing (e.g., à la Clause-Diffusion). A model for the representation of the parallel searches produced by such strategies is presented, and the bounded-search-spaces approach to the measurement of search complexity in infinite search spaces is extended to distributed search. This involves capturing both its advantages, e.g., the subdivision of work, and disadvantages, e.g., the cost of communication, in terms of search space. These tools are applied to compare the evolution of the search space of a contraction-based strategy with that of its parallelization in the above sense
Proof Generation in CDSAT
Full text linkThe main ideas in the CDSAT (Conflict-Driven Satisfiability) framework for SMT are summarized, leading to approaches to proof generation in CDSAT
Towards a unified model of search in theorem-proving: subgoal-reduction strategies
Full text linkAbstractThis paper advances the design of a unified model for the representation of search in first-order clausal theorem-proving, by extending to tableau-based subgoal-reduction strategies (e.g., model-elimination tableaux), the marked search-graph model, already introduced for ordering-based strategies, those that use (ordered) resolution, paramodulation/superposition, simplification, and subsumption. The resulting analytic marked search-graphs subsume AND–OR graphs, and allow us to represent those dynamic components, such as backtracking and instantiation of rigid variables, that have long been an obstacle to modelling subgoal-reduction strategies properly. The second part of the paper develops for analytic marked search-graphs the bounded search spaces approach to the analysis of infinite search spaces. We analyze how tableau inferences and backtracking affect the bounded search spaces during a derivation. Then, we apply this analysis to measure the effects of regularity and lemmatization by folding-up on search complexity, by comparing the bounded search spaces of strategies with and without these features. We conclude with a discussion comparing the marked search-graphs for tableaux, linear resolution, and ordering-based strategies, showing how this search model applies across these classes of strategies
- …
