It is common for formal methods to receive a set of lemmas as input. It could be for compiler optimization, program verification, or program synthesis. Creating such a set requires expert engineers and is difficult to maintain in a growing code-base. This work focuses on automatically discovering and proving lemmas, using a novel deductive approach. By using a deductive approach, terms can be represented by symbolic terms (where variables are universally quantified). Symbolic terms can then represent any object, whether it is a database or a function, without incurring long runtimes. The evaluation shows this method to be superior to prior-art both in run-time and in the lemmas collected.
Speech to text software is a valuable tool for the hearing impaired. It enables them to attend lectures with real-time transcription. A common issue in such lectures is the vocabulary where missing words will lead to errors in transcription. Speech to text techniques traditionally are built from three models, a physical model for processing sounds, a phonetic model to translate sounds to a phonetic word\sentence, and finally the language model. The language model translates the phonetics to words, using the vocabulary and some statistical model. By creating a custom vocabulary from Wikipedia we both get a relevant vocabulary and a context-aware statistical model which leads to a decrease in transcription error rate.
created with
Website Design Software .