Theorem proving for intensional logic

DOI10.1007/BF00881857zbMATH Open1430.68420OpenAlexW1995457855MaRDI QIDQ1891256FDOQ1891256

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

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

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Generating relevant models
• A theory of properties
• Title not available (Why is that?)

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
• Title not available (Why is that?)
• Dynamic logic as a uniform framework for theorem proving in intensional logic
• Title not available (Why is that?)

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)