Efficient model generation through compilation. (Q1854374): Difference between revisions

@@ Property / full work available at URL @@
+https://doi.org/10.1006/inco.1999.2863
+Normal rank
@@ Property / OpenAlex ID @@
+W2066884140
@@ Property / OpenAlex ID: W2066884140 / rank @@
+Normal rank
@@ Property / cites work @@
+Hyper tableaux
@@ Property / cites work: Hyper tableaux / rank @@
+Normal rank
@@ Property / cites work @@
+LeanT A P: Lean tableau-based theorem proving
@@ Property / cites work: LeanT A P: Lean tableau-based theorem proving / rank @@
+Normal rank
@@ Property / cites work @@
+Minimal model generation with positive unit hyper-resolution tableaux
+Normal rank
@@ Property / cites work @@
+Q4287493
@@ Property / cites work: Q4287493 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5688908
@@ Property / cites work: Q5688908 / rank @@
+Normal rank
@@ Property / cites work @@
+Hyperresolution and automated model building
@@ Property / cites work: Hyperresolution and automated model building / rank @@
+Normal rank
@@ Property / cites work @@
+Q4524770
@@ Property / cites work: Q4524770 / rank @@
+Normal rank
@@ Property / cites work @@
+SATCHMORE: SATCHMO with RElevancy
@@ Property / cites work: SATCHMORE: SATCHMO with RElevancy / rank @@
+Normal rank
@@ Property / cites work @@
+Q3821629
@@ Property / cites work: Q3821629 / rank @@
+Normal rank
@@ Property / cites work @@
+A Prolog technology theorem prover: Implementation by an extended Prolog compiler
+Normal rank
@@ Property / cites work @@
+The TPTP problem library
@@ Property / cites work: The TPTP problem library / rank @@
+Normal rank
@@ Property / cites work @@
+The design of the CADE-13 ATP system competition
@@ Property / cites work: The design of the CADE-13 ATP system competition / rank @@
+Normal rank
@@ Property / cites work @@
+Using resolution for deciding solvable classes and building finite models
+Normal rank