bfjviiDec 22, 2023
Check out the demo for Lean Verbose https://github.com/PatrickMassot/lean-verbose #lean4 #theorem_proving
GitHub - PatrickMassot/lean-verbose: Very controlled natural language tactics for Lean

Very controlled natural language tactics for Lean. Contribute to PatrickMassot/lean-verbose development by creating an account on GitHub.

GitHub
nopeNov 21, 2023
Social and Semiotic Analyses for Theorem Prover User Interface Design 1, Volume 11
(1999) Goguen, Joseph
Url: http://dx.doi.org/10.1007/s001650050051
#my_bibtex #Kumo #interface_design #semiotics #social_computing #theorem_proving
Social and Semiotic Analyses for Theorem Prover User Interface Design 1 | Formal Aspects of Computing

Abstract. We describe an approach to user interface design based on ideas from social science, narratology (the theory of stories), cognitive science, and a new area called algebraic semiotics. Social analysis helps to identify certain roles for users ...

Formal Aspects of Computing
nopeOct 2, 2023
A Framework for Defining Logics
(1993) : Harper, Robert Honsell, Furio ...
DOI: https://doi.org/10.1145/138027.138060
#LF #lambda_calculus #proof_search #theorem_proving #judgement #edinburgh_logical_framework #formal_methods #my_bibtex
A framework for defining logics | Journal of the ACM

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more ...

Journal of the ACM
nopeOct 2, 2023
The Semantics of Clocks
(1988) : Smith, Brian Cantwell
DOI: https://doi.org/10.1007/978-94-009-2699-8
#theorem_proving #clocks #ontology #time_keeping #semantics #time #typology #diagram #my_bibtex
nopeSep 23, 2023
A Framework for Defining Logics
(1993) : Harper, Robert Honsell, Furio ...
DOI: https://doi.org/10.1145/138027.138060
#edinburgh_logical_framework #formal_methods #lambda_calculus #theorem_proving #LF #judgement #proof_search #my_bibtex
A framework for defining logics | Journal of the ACM

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more ...

Journal of the ACM
nopeSep 19, 2023
A Framework for Defining Logics
(1993) : Harper, Robert Honsell, Furio ...
DOI: https://doi.org/10.1145/138027.138060
#edinburgh_logical_framework #LF #lambda_calculus #formal_methods #theorem_proving #judgement #proof_search #my_bibtex
A framework for defining logics | Journal of the ACM

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more ...

Journal of the ACM
nopeAug 22, 2023
Nonmonotonic Reasoning
(1991) : Brewka, Gerhard
isbn: 0-521-38394-3
#logic #default_logic #inheritance_systems #preferred_semantics #theorem_proving #rule_system #circumscription #nonmonotonic_reasoning #my_bibtex
nopeAug 19, 2023
Social and Semiotic Analyses for Theorem Prover User Interface Design 1
(1999) : Goguen, Joseph
DOI: https://doi.org/10.1007/s001650050051
#theorem_proving #Kumo #semiotics #interface_design #social_computing #my_bibtex
Social and Semiotic Analyses for Theorem Prover User Interface Design 1 | Formal Aspects of Computing

Abstract. We describe an approach to user interface design based on ideas from social science, narratology (the theory of stories), cognitive science, and a new area called algebraic semiotics. Social analysis helps to identify certain roles for users ...

Formal Aspects of Computing
nopeAug 14, 2023
The Semantics of Clocks
(1988) : Smith, Brian Cantwell
DOI: https://doi.org/10.1007/978-94-009-2699-8
#clocks #typology #time #diagram #ontology #theorem_proving #time_keeping #semantics #my_bibtex
nopeAug 8, 2023
The Semantics of Clocks
(1988) : Smith, Brian Cantwell
DOI: https://doi.org/10.1007/978-94-009-2699-8
#diagram #semantics #ontology #clocks #typology #theorem_proving #time_keeping #time #my_bibtex