SET-VAR

DOI10.1007/BF00881869zbMath0802.68130OpenAlexW2914221638MaRDI QIDQ1319383

Guohui Feng, W. W. Bledsoe

Publication date: 12 April 1994

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

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

zbMATH Keywords

second-order logiccircumscriptionset-theory

Mathematics Subject Classification ID

Related Items

TPS: A hybrid automatic-interactive system for developing proofs, TPS: A theorem-proving system for classical type theory, Solving equations with sequence variables and sequence functions, The calculus of constructions as a framework for proof search with set variable instantiation, Reducing higher-order theorem proving to a sequence of SAT problems

Uses Software

• OTTER
• METEOR

Cites Work

• Eliminating dublication with the hyper-linking strategy
• On connections and higher-order logic
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Circumscription - a form of non-monotonic reasoning
• A man-machine theorem-proving system
• Solvable cases of the decision problem
• A Machine-Oriented Logic Based on the Resolution Principle
• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• Unnamed Item
• Unnamed Item
• Unnamed Item