Pages that link to "Item:Q3994754"

The following pages link to Automated reasoning: 33 research problems (Q3994754):

Displaying 49 items.

• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization (Q286801) (← links)
• Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\) (Q545319) (← links)
• The problem of demodulator adjunction (Q688566) (← links)
• A systematic methodology for automated theorem finding (Q744079) (← links)
• Basic research problems: The problem of choosing the representation, inference rule, and strategy (Q809627) (← links)
• The problem of choosing the type of subsumption to use (Q809628) (← links)
• Meeting the challenge of fifty years of logic (Q911807) (← links)
• Automated proof of ring commutativity problems by algebraic methods (Q912612) (← links)
• A resolution framework for finitely-valued first-order logics (Q1185455) (← links)
• Some experiments with a completion theorem prover (Q1186705) (← links)
• Resolution approximation of first-order logics (Q1187026) (← links)
• A method for simultaneous search for refutations and models by equational constraint solving (Q1198235) (← links)
• A new subsumption method in the connection graph proof procedure (Q1199542) (← links)
• The problem of naming and function replacement (Q1311398) (← links)
• The kernel strategy and its use for the study of combinatory logic (Q1311399) (← links)
• The problem of reasoning by analogy (Q1311406) (← links)
• The problem of selecting an approach based on prior success (Q1311414) (← links)
• The problem of automated theorem finding (Q1312164) (← links)
• The problem of induction (Q1319388) (← links)
• The problem of reasoning by case analysis (Q1319394) (← links)
• Basic research problems: The problem of strategy and hyperresolution (Q1332645) (← links)
• The problem of hyperparamodulation (Q1337565) (← links)
• The problem of hyperparamodulation and nuclei (Q1340968) (← links)
• The application of automated reasoning to questions in mathematics and logic (Q1354049) (← links)
• Clause trees: A tool for understanding and implementing resolution in automated reasoning (Q1402732) (← links)
• An overview of automated reasoning and related fields (Q1819948) (← links)
• The problem of guaranteeing the existence of a complete set of reductions (Q1823015) (← links)
• Searching for circles of pure proofs (Q1904397) (← links)
• A finitely axiomatized formalization of predicate calculus with equality (Q1906674) (← links)
• Avoiding duplicate proofs with the foothold refinement (Q1924821) (← links)
• Solving SAT by algorithm transform of Wu's method (Q1966110) (← links)
• Larry Wos: visions of automated reasoning (Q2102922) (← links)
• A Wos Challenge Met (Q2102924) (← links)
• Finding proofs in Tarskian geometry (Q2362499) (← links)
• Ideal resolution principle for lattice-valued first-order logic based on lattice implication algebra (Q2440194) (← links)
• Unnecessary inferences in associative-commutative completion procedures (Q3489486) (← links)
• Accepting/rejecting propositions from accepted/rejected propositions: A unifying overview (Q3537540) (← links)
• Removing irrelevant information in temporal resolution proofs (Q4421286) (← links)
• (Q4823613) (← links)
• Layered map reasoning (Q4923516) (← links)
• Consider only general superpositions in completion procedures (Q5055743) (← links)
• Problems in rewriting III (Q5055847) (← links)
• Building Theorem Provers (Q5191110) (← links)
• Building proofs or counterexamples by analogy in a resolution framework (Q5235252) (← links)
• Proving group isomorphism theorems (Q5881193) (← links)
• \(\alpha\)-resolution principle based on lattice-valued propositional logic \(\text{LP} (X)\) (Q5946276) (← links)
• An examination of the prolog technology theorem-prover (Q6488542) (← links)
• A mechanically assisted constructive proof in category theory (Q6488555) (← links)
• Minimizing the number of clauses by renaming (Q6488560) (← links)