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

@@ Property / Mathematics Subject Classification ID @@
+Q60
@@ Property / Mathematics Subject Classification ID: 68Q60 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+T15
@@ Property / Mathematics Subject Classification ID: 68T15 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+T27
@@ Property / Mathematics Subject Classification ID: 68T27 / rank @@
+Normal rank
@@ Property / Mathematics Subject Classification ID @@
+B15
@@ Property / Mathematics Subject Classification ID: 03B15 / rank @@
+Normal rank
@@ Property / zbMATH DE Number @@
+6367493
@@ Property / zbMATH DE Number: 6367493 / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+HOL theorem prover
@@ Property / zbMATH Keywords: HOL theorem prover / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+multiway decision graphs
@@ Property / zbMATH Keywords: multiway decision graphs / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+reduction techniques
@@ Property / zbMATH Keywords: reduction techniques / rank @@
+Normal rank
@@ Property / zbMATH Keywords @@
+soundness
@@ Property / zbMATH Keywords: soundness / rank @@
+Normal rank
@@ 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
@@ links / mardi / name / links / mardi / name @@
+Publication:469363