The application of automated reasoning to questions in mathematics and logic
type: Item
instance of: scholarly article
title: The application of automated reasoning to questions in mathematics and logic
zbMATH Open document ID: 0997.03500
DOI: 10.1007/BF01543481
author: Larry Wos
author: William McCune
published in: Annals of Mathematics and Artificial Intelligence
publication date: 1997-05-13T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03-04
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1005848
zbMATH Keywords: automated reasoning
zbMATH Keywords: OTTER
zbMATH Keywords: proof finding
zbMATH Keywords: conjecture formulation
zbMATH Keywords: object construction
zbMATH Keywords: combinatory logic
zbMATH Keywords: equivalential calculus
zbMATH Keywords: Robbins algebra
zbMATH Keywords: finite semigroup
describes a project that uses: OTTER
describes a project that uses: SbReve2
describes a project that uses: AURA
describes a project that uses: NQTHM
describes a project that uses: RRL
MaRDI profile type: Publication
Wikidata QID: Q114267028
cites work: The lambda calculus, its syntax and semantics
cites work: Proof Checking the RSA Public Key Encryption Algorithm
cites work: Q4040283
cites work: Q5649989
cites work: Q5616133
cites work: New Sets of Independent Postulates for the Algebra of Logic, With Special Reference to Whitehead and Russell's Principia Mathematica
cites work: A shortest single axiom for the classical equivalential calculus
cites work: Q5581665
cites work: Using automated reasoning tools: A study of the semigroup \(F_ 2B_ 2\)
cites work: Complexity and related enhancements for automated theorem-proving programs
cites work: A case study in automated theorem proving: Finding sages in combinatory logic
cites work: Experiments with discrimination-tree indexing and path indexing for term retrieval
cites work: Q5624683
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q5541351
cites work: A Prolog technology theorem prover: Implementation by an extended Prolog compiler
cites work: Semigroups, Antiautomorphisms, and Involutions: A Computer Solution to an Open Problem, I
cites work: Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
cites work: The Concept of Demodulation in Theorem Proving
cites work: Q3829089
cites work: A new use of an automated reasoning assistant: Open questions in equivalential calculus an the study of infinite domains
cites work: Q3994754
cites work: Erratum to ``A case study in automated theorem proving: finding sages in combinatory logic''
cites work: Meeting the challenge of fifty years of logic
description: scientific article; zbMATH DE number 1005848