Searched refs:logic (Results 1 - 25 of 253) sorted by relevance

1234567891011

/seL4-l4v-master/HOL4/Manual/Logic/
H A DMakefile14 ps: logic.ps
15 pdf: logic.pdf
18 rm -f *.dvi *.aux *.toc *.log *.bbl *.blg logic.pdf logic.ps
20 logic.pdf: logic.tex $(CHAPTERS) $(OTHER)
21 ${PDFLATEX} logic
22 ${BIBTEX} logic
23 ${PDFLATEX} logic
24 ${PDFLATEX} logic
[all...]
H A Dsyntax.tex7 \chapter{Syntax and Semantics}\label{logic}
13 logic supported by the \HOL{} system, which is a variant of
15 will henceforth be called the \HOL{} logic, or just \HOL. The
18 of this description is the \HOL{} logic. Note that there is a
20 logic, namely the programming language \ML. This is the language used
21 to manipulate the \HOL{} logic by users of the system. It is hoped
35 universe\/}\index{universe, in semantics of HOL logic@universe, in
36 semantics of \HOL{} logic} and which is assumed to have the following
106 \theory{ZFC} set theory of the semantics of the \HOL{} logic to be given
112 The types\index{type constraint!in HOL logic
[all...]
H A Dpreface.tex4 This volume contains the description of the \HOL\ system's logic. It
8 \item \LOGIC: a formal description of the higher order logic
19 logic in terms of a set-theoretic semantics. This material was
21 \DESCRIPTION. Because this logic is shared with other theorem-proving
27 higher order logic (hence the acronym `\HOL'). To this end, the formal
28 logic is interfaced to a general purpose programming language (\ML, for
29 meta-language) in which terms and theorems of the logic can be denoted,
31 The version of higher order logic used in \HOL\ is predicate calculus
36 (The use of higher order logic for this purpose was first advocated by
37 Keith Hanna \cite{Hanna-Daeche}.) However, the logic doe
[all...]
/seL4-l4v-master/isabelle/src/Pure/ML/
H A Dml_console.scala19 var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
31 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
37 Build a logic session image and run the raw Isabelle ML process
43 "l:" -> (arg => logic = arg),
53 // build logic
58 Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
65 ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
72 options, logic, dir
[all...]
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/
H A Dml_console.scala19 var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
31 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
37 Build a logic session image and run the raw Isabelle ML process
43 "l:" -> (arg => logic = arg),
53 // build logic
58 Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
65 ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
72 options, logic, dir
[all...]
/seL4-l4v-master/HOL4/Manual/
H A DMakefile19 Logic/logic.pdf:
44 logic: Logic/logic.pdf
50 all: description tutorial logic reference interaction quick
/seL4-l4v-master/graph-refine/example/
H A Dtarget.py12 import logic namespace
34 pair = logic.mk_pairing (functions, f, f2)
/seL4-l4v-master/graph-refine/loop-example/synth/
H A Dtarget.py12 import logic namespace
34 pair = logic.mk_pairing (functions, f, f2)
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dbuild_docker.scala28 logic: String = default_logic,
69 perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
70 Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \
107 var logic = default_logic
123 -l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
130 Build Isabelle docker image with default logic image, using a standard
140 "l:" -> (arg => logic = arg),
154 build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
H A Dupdate.scala12 def update(options: Options, logic: String,
23 context.build_logic(logic)
41 context.sessions(logic, log = log).foreach(_.process((args: Dump.Args) =>
75 var logic = Dump.default_logic
89 -b NAME base logic image (default """ + isabelle.quote(Dump.default_logic) + """)
104 "b:" -> (arg => logic = arg),
117 update(options, logic,
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dbuild_docker.scala28 logic: String = default_logic,
69 perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
70 Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \
107 var logic = default_logic
123 -l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
130 Build Isabelle docker image with default logic image, using a standard
140 "l:" -> (arg => logic = arg),
154 build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
H A Dupdate.scala12 def update(options: Options, logic: String,
23 context.build_logic(logic)
41 context.sessions(logic, log = log).foreach(_.process((args: Dump.Args) =>
75 var logic = Dump.default_logic
89 -b NAME base logic image (default """ + isabelle.quote(Dump.default_logic) + """)
104 "b:" -> (arg => logic = arg),
117 update(options, logic,
/seL4-l4v-master/HOL4/examples/ind_def/
H A DmilScript.sml4 (* logic, and proves the Curry-Howard isomorphism for *)
5 (* this and typed combinatory logic. *)
24 (* Combinatory logic types and type judgements. *)
35 (* Definition of well-typed terms of combinatory logic. *)
49 (* Mimimal intuitionistic logic. We now reinterpret -> as implication, *)
50 (* types P:('a)ty as terms of the logic (i.e. propositions), and define a *)
52 (* inductively by the proof rules for the logic. *)
/seL4-l4v-master/isabelle/src/Pure/System/
H A Disabelle_process.scala17 logic: String = "",
31 Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
38 logic: String = "",
55 ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
/seL4-l4v-master/l4v/isabelle/src/Pure/System/
H A Disabelle_process.scala17 logic: String = "",
31 Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
38 logic: String = "",
55 ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/
H A Dbuild_vscode.scala22 val logic = Grammar.default_logic
23 val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords
25 val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
H A Dgrammar.scala19 def default_output(logic: String = ""): String =
20 if (logic == "" || logic == default_logic) "isabelle-grammar.json"
21 else "isabelle-" + logic + "-grammar.json"
140 var logic = default_logic
148 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
154 "l:" -> (arg => logic = arg),
161 Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords
162 val output_path = output getOrElse Path.explode(default_output(logic))
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/
H A Dbuild_vscode.scala22 val logic = Grammar.default_logic
23 val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords
25 val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
H A Dgrammar.scala19 def default_output(logic: String = ""): String =
20 if (logic == "" || logic == default_logic) "isabelle-grammar.json"
21 else "isabelle-" + logic + "-grammar.json"
140 var logic = default_logic
148 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
154 "l:" -> (arg => logic = arg),
161 Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords
162 val output_path = output getOrElse Path.explode(default_output(logic))
/seL4-l4v-master/graph-refine/loop-example/O1/
H A Dtarget.py14 import logic namespace
33 assert logic.aligned_address_sanity (afunctions, symbols, 4)
/seL4-l4v-master/graph-refine/seL4-example/
H A Dtarget.py14 import logic namespace
31 assert logic.aligned_address_sanity (afunctions, symbols, 4)
41 print 'Doing stack/inst logic.'
/seL4-l4v-master/graph-refine/loop-example/O2/
H A Dtarget.py14 import logic namespace
33 assert logic.aligned_address_sanity (afunctions, symbols, 4)
/seL4-l4v-master/HOL4/examples/Hoare-for-divergence/
H A Dstd_logicScript.sml5 (* -- inference rules for a standard total-correctness Hoare logic -- *)
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/
H A Ddataabs.ml5 % logic to boolean logic for single bits and for %
10 % logic to booleans. The predicates Def and Defn %
12 % ways of abstracting to boolean logic would include %
14 % three-valued logic consisting of T,F and bottom. %
/seL4-l4v-master/HOL4/Manual/Description/
H A Dpreface.tex8 \item \LOGIC: a formal description of the higher order logic
23 higher order logic (hence the acronym `\HOL'). To this end, the formal
24 logic is interfaced to a general purpose programming language (\ML, for
25 meta-language) in which terms and theorems of the logic can be denoted,
27 The version of higher order logic used in \HOL\ is predicate calculus
32 (The use of higher order logic for this purpose was first advocated by
33 Keith Hanna \cite{Hanna-Daeche}.) However, the logic does not restrict
36 This document presents the \HOL\ logic in its \ML{} guise, and
38 generate proofs in the logic. Thus, it describes how the abstract
45 the language \ML. That work centred on a system called \LCF\ (logic fo
[all...]

Completed in 185 milliseconds

1234567891011