Theorem proving for intensional logic

DOI10.1007/BF00881857MaRDI QIDQ1891256zbMATH OpenOpenAlexFDO

Authors Allan Ramsay

Publication date 22 November 1995

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

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

Mathematics Subject Classification ID

Knowledge representation (68T30) Logic of natural languages (03B65) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Constructing a normal form for property theory
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application
• Dynamic logic as a uniform framework for theorem proving in intensional logic
• An Intuitionistic Predicate Logic Theorem Prover
• A family of goal directed theorem provers based on conjunction and implication. I

Cites work

• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• scientific article; zbMATH DE number 43239 (Why is no real title available?)
• scientific article; zbMATH DE number 2188308 (Why is no real title available?)
• A theory of properties
• Generating relevant models

Cited in

(7)

• Proof internalization in generalized Frege systems for classical logic
• Theorem proving for untyped constructive \(\lambda\)-calculus: Implementation and application
• Constructing a normal form for property theory
• A resolution theorem prover for intuitionistic logic
• scientific article; zbMATH DE number 5235522 (Why is no real title available?)
• Dynamic logic as a uniform framework for theorem proving in intensional logic
• scientific article; zbMATH DE number 54243 (Why is no real title available?)

This page was built for publication: Theorem proving for intensional logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1891256)