Automatic verification of reduction techniques in higher order logic (Q469363): Difference between revisions

@@ Property / describes a project that uses @@
+MiniSat
@@ Property / describes a project that uses: MiniSat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+InVeSt
@@ Property / describes a project that uses: InVeSt / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ACL2
@@ Property / describes a project that uses: ACL2 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+ML
@@ Property / describes a project that uses: ML / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL
@@ Property / describes a project that uses: HOL / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MDGs
@@ Property / describes a project that uses: MDGs / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Uppaal
@@ Property / describes a project that uses: Uppaal / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s00165-012-0223-x
+Normal rank
@@ Property / OpenAlex ID @@
+W2007666139
@@ Property / OpenAlex ID: W2007666139 / rank @@
+Normal rank
@@ Property / cites work @@
+Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover
+Normal rank
@@ Property / cites work @@
+On the non-termination of MDG-based abstract state enumeration
+Normal rank
@@ Property / cites work @@
+Deciding Bit-Vector Arithmetic with Abstraction
@@ Property / cites work: Deciding Bit-Vector Arithmetic with Abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Graph-Based Algorithms for Boolean Function Manipulation
+Normal rank
@@ Property / cites work @@
+Introduction to the OBDD algorithm for the ATP community
+Normal rank
@@ Property / cites work @@
+Q4885877
@@ Property / cites work: Q4885877 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4720771
@@ Property / cites work: Q4720771 / rank @@
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Edinburgh LCF. A mechanized logic of computation
@@ Property / cites work: Edinburgh LCF. A mechanized logic of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Equational Abstractions for Reducing the State Space of Rewrite Theories
+Normal rank
@@ Property / cites work @@
+Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs (MDGs)
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Q4494394
@@ Property / cites work: Q4494394 / rank @@
+Normal rank
@@ Property / cites work @@
+Equational abstractions
@@ Property / cites work: Equational abstractions / rank @@
+Normal rank
@@ Property / cites work @@
+Q2754105
@@ Property / cites work: Q2754105 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3700812
@@ Property / cites work: Q3700812 / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic model checking for real-time systems
@@ Property / cites work: Symbolic model checking for real-time systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q4037380
@@ Property / cites work: Q4037380 / rank @@
+Normal rank