Class information for:
Level 1: THEOREM PROVING//SYMBOLIC TRAJECTORY EVALUATION//MULTIWAY DECISION GRAPHS

Basic class information

Class id #P Avg. number of
references
Database coverage
of references
18723 538 24.0 23%



Bar chart of Publication_year

Last years might be incomplete

Hierarchy of classes

The table includes all classes above and classes immediately below the current class.



Cluster id Level Cluster label #P
9 4 COMPUTER SCIENCE, THEORY & METHODS//COMPUTER SCIENCE, ARTIFICIAL INTELLIGENCE//COMPUTER SCIENCE, INFORMATION SYSTEMS 1247339
148 3       COMPUTER SCIENCE, SOFTWARE ENGINEERING//COMPUTER SCIENCE, THEORY & METHODS//ACM SIGPLAN NOTICES 63683
708 2             COMPUTER SCIENCE, THEORY & METHODS//JOURNAL OF AUTOMATED REASONING//LAMBDA CALCULUS 12890
18723 1                   THEOREM PROVING//SYMBOLIC TRAJECTORY EVALUATION//MULTIWAY DECISION GRAPHS 538

Terms with highest relevance score



rank Term termType Chi square Shr. of publ. in
class containing
term
Class's shr. of
term's tot. occurrences
#P with
term in
class
1 THEOREM PROVING authKW 333055 8% 13% 45
2 SYMBOLIC TRAJECTORY EVALUATION authKW 309002 1% 78% 7
3 MULTIWAY DECISION GRAPHS authKW 291886 1% 86% 6
4 ACL2 authKW 270417 2% 53% 9
5 HARDWARE VERIFICATION authKW 245926 2% 33% 13
6 HOL THEOREM PROVER authKW 151347 1% 67% 4
7 STRATEG CAD S address 149851 2% 20% 13
8 JOURNAL OF AUTOMATED REASONING journal 149409 8% 6% 43
9 INTERACTIVE THEOREM PROVING authKW 143140 2% 19% 13
10 FORMAL VERIFICATION authKW 136088 7% 6% 39

Web of Science journal categories



Rank Term Chi square Shr. of publ. in
class containing
term
Class's shr. of
term's tot. occurrences
#P with
term in
class
1 Computer Science, Theory & Methods 20979 54% 0% 291
2 Computer Science, Software Engineering 7542 28% 0% 148
3 Computer Science, Hardware & Architecture 6144 19% 0% 103
4 Computer Science, Information Systems 2769 19% 0% 102
5 Computer Science, Artificial Intelligence 1781 15% 0% 83
6 Logic 1509 4% 0% 20
7 Mathematics, Applied 122 7% 0% 39
8 Engineering, Electrical & Electronic 83 10% 0% 53
9 Computer Science, Interdisciplinary Applications 62 4% 0% 19
10 Engineering, General 5 1% 0% 7

Address terms



Rank Term Chi square Shr. of publ. in
class containing
term
Class's shr. of
term's tot. occurrences
#P with
term in
class
1 STRATEG CAD S 149851 2% 20% 13
2 BEIJING ELECT SYST RELIABIL TECHNOL 129725 1% 57% 4
3 ASP ADV TOOLS METHODOL GRP 113512 0% 100% 2
4 PERFORMANCE MICROPROCESSOR 113512 0% 100% 2
5 SOMERSET POWERPC DESIGN 102158 1% 60% 3
6 ARCHITECTURE SYST PLATFORMS 75673 0% 67% 2
7 CIENCIA COMP MATEMAT 75673 0% 67% 2
8 ABT F DATENBANKEN ARTIFICIAL INTELLIGENCE 56756 0% 100% 1
9 ARBEITSGRP LOG MAT GRUNDLAGEN INFORMAT 56756 0% 100% 1
10 ASP ADV TOOLS METHODOL 56756 0% 100% 1

Journals



Rank Term Chi square Shr. of publ. in
class containing
term
Class's shr. of
term's tot. occurrences
#P with
term in
class
1 JOURNAL OF AUTOMATED REASONING 149409 8% 6% 43
2 FORMAL METHODS IN SYSTEM DESIGN 130634 6% 7% 34
3 LECTURE NOTES IN COMPUTER SCIENCE 25213 37% 0% 198
4 FORMAL ASPECTS OF COMPUTING 9419 1% 2% 8
5 JOURNAL OF FUNCTIONAL PROGRAMMING 4424 1% 2% 5
6 MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE 3880 1% 1% 6
7 JOURNAL OF APPLIED LOGIC 3745 1% 2% 4
8 IEEE DESIGN & TEST OF COMPUTERS 3672 1% 1% 8
9 SCIENCE OF COMPUTER PROGRAMMING 3503 2% 1% 10
10 JOURNAL OF SYMBOLIC COMPUTATION 3028 2% 0% 11

Author Key Words



Rank Term Chi square Shr. of publ. in
class containing
term
Class's shr. of
term's tot. occurrences
#P with
term in
class
LCSH search Wikipedia search
1 THEOREM PROVING 333055 8% 13% 45 Search THEOREM+PROVING Search THEOREM+PROVING
2 SYMBOLIC TRAJECTORY EVALUATION 309002 1% 78% 7 Search SYMBOLIC+TRAJECTORY+EVALUATION Search SYMBOLIC+TRAJECTORY+EVALUATION
3 MULTIWAY DECISION GRAPHS 291886 1% 86% 6 Search MULTIWAY+DECISION+GRAPHS Search MULTIWAY+DECISION+GRAPHS
4 ACL2 270417 2% 53% 9 Search ACL2 Search ACL2
5 HARDWARE VERIFICATION 245926 2% 33% 13 Search HARDWARE+VERIFICATION Search HARDWARE+VERIFICATION
6 HOL THEOREM PROVER 151347 1% 67% 4 Search HOL+THEOREM+PROVER Search HOL+THEOREM+PROVER
7 INTERACTIVE THEOREM PROVING 143140 2% 19% 13 Search INTERACTIVE+THEOREM+PROVING Search INTERACTIVE+THEOREM+PROVING
8 FORMAL VERIFICATION 136088 7% 6% 39 Search FORMAL+VERIFICATION Search FORMAL+VERIFICATION
9 NQTHM 129725 1% 57% 4 Search NQTHM Search NQTHM
10 COMPLETION FUNCTIONS 113512 0% 100% 2 Search COMPLETION+FUNCTIONS Search COMPLETION+FUNCTIONS

Core articles

The table includes core articles in the class. The following variables is taken into account for the relevance score of an article in a cluster c:
(1) Number of references referring to publications in the class.
(2) Share of total number of active references referring to publications in the class.
(3) Age of the article. New articles get higher score than old articles.
(4) Citation rate, normalized to year.



Rank Reference # ref.
in cl.
Shr. of ref. in
cl.
Citations
1 BOLDO, S , LELAY, C , MELQUIOND, G , (2016) FORMALIZATION OF REAL ANALYSIS: A SURVEY OF PROOF ASSISTANTS AND LIBRARIES.MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE. VOL. 26. ISSUE 7. P. 1196 -1233 22 79% 0
2 SEGER, CJH , JONES, RB , O'LEARY, JW , MELHAM, T , AAGAARD, MD , BARRETT, C , SYME, D , (2005) AN INDUSTRIALLY EFFECTIVE ENVIRONMENT FOR FORMAL HARDWARE VERIFICATION.IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS. VOL. 24. ISSUE 9. P. 1381-1405 16 89% 32
3 FOX, AJC , HARMAN, NA , (2003) ALGEBRAIC MODELS OF CORRECTNESS FOR ABSTRACT PIPELINES.JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING. VOL. 57. ISSUE 1-2. P. 71-107 14 100% 9
4 AKBARPOUR, B , ABDEL-HAMID, AT , TAHAR, S , HARRISON, J , (2010) VERIFYING A SYNTHESIZED IMPLEMENTATION OF IEEE-754 FLOATING-POINT EXPONENTIAL FUNCTION USING HOL.COMPUTER JOURNAL. VOL. 53. ISSUE 4. P. 465 -488 13 81% 5
5 AKBARPOUR, B , TAHAR, S , DEKDOUK, A , (2005) FORMALIZATION OF FIXED-POINT ARITHMETIC IN HOL.FORMAL METHODS IN SYSTEM DESIGN. VOL. 27. ISSUE 1-2. P. 173 -200 12 100% 6
6 MANOLIOS, P , (2006) REFINEMENT AND THEOREM PROVING.FORMAL METHODS FOR HARDWARE VERIFICATION. VOL. 3965. ISSUE . P. 176 -210 11 100% 0
7 HOSABETTU, R , GOPALAKRISHNAN, G , SRIVAS, M , (2003) FORMAL VERIFICATION OF A COMPLEX PIPELINED PROCESSOR.FORMAL METHODS IN SYSTEM DESIGN. VOL. 23. ISSUE 2. P. 171 -213 11 100% 11
8 KAUFMANN, M , MOORE, JS , RAY, S , REEBER, E , (2009) INTEGRATING EXTERNAL DEDUCTION TOOLS WITH ACL2.JOURNAL OF APPLIED LOGIC. VOL. 7. ISSUE 1. P. 3 -25 10 91% 2
9 HUNT, WA , (2004) MECHANICAL MATHEMATICAL METHODS FOR MICROPROCESSOR VERIFICATION.COMPUTER AIDED VERIFICATION. VOL. 3114. ISSUE . P. 523 -533 10 100% 0
10 HARMAN, NA , (2007) ALGEBRAIC MODELS OF BEHAVIOUR AND CORRECTNESS OF SMT AND CMT PROCESSORS.JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING. VOL. 74. ISSUE 1. P. 32-56 10 83% 2

Classes with closest relation at Level 1



Rank Class id link
1 26372 PROOF PLANNING//DEDUCTIVE PROGRAM SYNTHESIS//PROOF PATCHING
2 6407 ABSTRACT INTERPRETATION//SEPARATION LOGIC//PREDICATE ABSTRACTION
3 9998 JOURNAL OF AUTOMATED REASONING//AUTOMATED THEOREM PROVING//MIZAR
4 14808 ORDERED BINARY DECISION DIAGRAMS//BINARY DECISION DIAGRAMS//BRANCHING PROGRAMS
5 20981 SOFTWARE BASED SELF TEST//FUNCTIONAL VERIFICATION//POST SILICON VALIDATION
6 8988 JOURNAL OF FUNCTIONAL PROGRAMMING//ACM SIGPLAN NOTICES//HASKELL
7 13930 ASSUME GUARANTEE REASONING//TEMPORAL LOGIC OF ACTIONS//COMPOSITIONAL REASONING
8 5920 MODEL CHECKING//TEMPORAL LOGIC//PARTIAL ORDER REDUCTION
9 7299 FORMAL ASPECTS OF COMPUTING//KLEENE ALGEBRA//EVENT B
10 25434 AMBITUS//CMOS TRANSISTOR NETWORKS//COMP BUSINESS GRP

Go to start page