A resolution theorem prover for intuitionistic logic (Q4647496): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1007/3-540-61511-3_65
+Normal rank
@@ Property / OpenAlex ID @@
+W1787768633
@@ Property / OpenAlex ID: W1787768633 / rank @@
+Normal rank
@@ Property / cites work @@
+Some applications of Gentzen's proof theory in automated deduction
+Normal rank
@@ Property / cites work @@
+Q5679729
@@ Property / cites work: Q5679729 / rank @@
+Normal rank
@@ Property / cites work @@
+Contraction-free sequent calculi for intuitionistic logic
+Normal rank
@@ Property / cites work @@
+Resolution methods for the decision problem
@@ Property / cites work: Resolution methods for the decision problem / rank @@
+Normal rank
@@ Property / cites work @@
+Q3972527
@@ Property / cites work: Q3972527 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4312461
@@ Property / cites work: Q4312461 / rank @@
+Normal rank
@@ Property / cites work @@
+The axioms of constructive geometry
@@ Property / cites work: The axioms of constructive geometry / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+An Intuitionistic Predicate Logic Theorem Prover
@@ Property / cites work: An Intuitionistic Predicate Logic Theorem Prover / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264720
@@ Property / cites work: Q4264720 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof strategies in linear logic
@@ Property / cites work: Proof strategies in linear logic / rank @@
+Normal rank
@@ Property / cites work @@
+Q4264724
@@ Property / cites work: Q4264724 / rank @@
+Normal rank
@@ Property / cites work @@
+The PRIZ system and propositional calculus
@@ Property / cites work: The PRIZ system and propositional calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999539
@@ Property / cites work: Q3999539 / rank @@
+Normal rank
@@ Property / cites work @@
+Investigations into proof-search in a system of first-order dependent function types
+Normal rank