Complexity and related enhancements for automated theorem-proving programs
From MaRDI portal
Publication:1229761
DOI10.1016/0898-1221(76)90002-XzbMath0336.68037OpenAlexW2036475963WikidataQ114262236 ScholiaQ114262236MaRDI QIDQ1229761
Publication date: 1976
Published in: Computers \& Mathematics with Applications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0898-1221(76)90002-x
Related Items
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic, Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures, The resonance strategy, The application of automated reasoning to questions in mathematics and logic, Searching for circles of pure proofs, The anatomy of vampire. Implementing bottom-up procedures with code trees, Axiomatizing the skew Boolean propositional calculus, Using hints to increase the effectiveness of an automated reasoning program: Case studies, Linear and unit-resulting refutations for Horn theories, Contradiction separation based dynamic multi-clause synergized automated deduction, Meeting the challenge of fifty years of logic, A resolution framework for finitely-valued first-order logics, Advanced indexing operations on substitution trees, Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning, Experiments with discrimination-tree indexing and path indexing for term retrieval, The problem of demodulator adjunction, The problem of demodulating across argument and literal boundaries, Canonical Ground Horn Theories, Refinements to depth-first iterative-deepening search in automatic theorem proving, Complete demodulation for automatic theorem proving, A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains, The application of automated reasoning to formal models of combinatorial optimization, The problem of naming and function replacement, The kernel strategy and its use for the study of combinatory logic, Basic research problems: The problem of choosing the representation, inference rule, and strategy, Uniform strategies: The CADE-11 theorem proving contest
Cites Work
