On connections and higher-order logic

DOI10.1007/BF00248320zbMath0694.03011OpenAlexW2040723389MaRDI QIDQ908896

Peter B. Andrews

Publication date: 1989

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00248320

zbMATH Keywords

connection methodexpansion treesproving theorems in Church's typed lambda-calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items

The higher-order prover \textsc{Leo}-II, Prolog Technology Reinforcement Learning Prover, TPS: A hybrid automatic-interactive system for developing proofs, Annual Meeting of the Association for Symbolic Logic, Pittsburgh, 1991, TPS: A theorem-proving system for classical type theory, Superposition for higher-order logic, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Machine learning guidance for connection tableaux, Superposition with lambdas, Superposition with lambdas, Superposition for full higher-order logic, Proof-search in type-theoretic languages: An introduction, A combinator-based superposition calculus for higher-order logic, SET-VAR

Uses Software

• ETPS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A compact representation of proofs
• Tautology testing with a generalized matrix reduction method
• Refutation graphs
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• A comparative study of several proof procedures
• Matings in matrices
• Theorem Proving via General Matings
• On Matrices with Connections
• Refutations by Matings
• False lemmas in Herbrand
• A supplement to Herbrand
• Resolution in type theory
• A formulation of the simple theory of types