scientific article
From MaRDI portal
Publication:3829089
zbMath0674.68057MaRDI QIDQ3829089
Jim Boyle, Larry Wos, Ross A. Overbeek, Ewing L. Lusk
Publication date: 1984
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Hybrid reasoning using universal attachment ⋮ Problem solving by searching for models with a theorem prover ⋮ Automated Reasoning in the Wild ⋮ Using automated reasoning tools: A study of the semigroup \(F_ 2B_ 2\) ⋮ A case study in automated theorem proving: Finding sages in combinatory logic ⋮ Running time experiments on some algorithms for solving propositional satisfiability problems ⋮ The application of automated reasoning to questions in mathematics and logic ⋮ Inconsistency check of a set of clauses using Petri net reductions ⋮ Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system ⋮ Using resolution for deciding solvable classes and building finite models ⋮ Solving problems with automated reasoning, expert systems and neural networks ⋮ Using tactics to reformulate formulae for resolution theorem proving ⋮ Propositional calculus problems in CHIP ⋮ Paraconsistency and word puzzles ⋮ Meeting the challenge of fifty years of logic ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Implementing the `Fool's model' of combinatory logic ⋮ The jobs puzzle: Taking on the challenge via controlled natural language processing ⋮ Reduction rules for resolution-based systems ⋮ On sets, types, fixed points, and checkerboards ⋮ Parsing as non-Horn deduction ⋮ A curious new result in switching theory ⋮ Structuring and automating hardware proofs in a higher-order theorem- proving environment ⋮ The search efficiency of theorem proving strategies ⋮ A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains ⋮ The problem of guaranteeing the existence of a complete set of reductions ⋮ Automated theorem proving methods ⋮ The absence and the presence of fixed point combinators ⋮ Basic research problems: The problem of choosing the representation, inference rule, and strategy ⋮ The problem of choosing the type of subsumption to use
