-
The impact of incoming preparation and demographics on performance in Physics I: a multi-institution comparison
Authors:
Shima Salehi,
Eric Burkholder,
G. Peter LePage,
Steven Pollock,
Carl Wieman
Abstract:
We have studied the impact of incoming preparation and demographic variables on student performance on the final exam in physics 1, the standard introductory, calculus-based mechanics course This was done at three different institutions using multivariable regression analysis to determine the extent to which exam scores can be predicted by a variety of variables that are available to most faculty…
▽ More
We have studied the impact of incoming preparation and demographic variables on student performance on the final exam in physics 1, the standard introductory, calculus-based mechanics course This was done at three different institutions using multivariable regression analysis to determine the extent to which exam scores can be predicted by a variety of variables that are available to most faculty and departments. We have found that the results are surprisingly consistent across the institutions, with the only two variables that have predictive power being math SAT/ACT scores and concept inventory pre-scores. The importance of both variables is comparable and fairly similar across the institutions. They explain 20 - 30 percent of the variation in students' performance on the final exam. Most notably, the demographic variables (gender, under-represented minority, first generation to attend college) are not significant. In all cases, although there appear to be gaps in exam performance if one considers only the demographic variable, once these two proxies of incoming preparation are included in the model, there is no longer a demographic gap. There is only a preparation gap that applies equally across the entire student population. This work shows that to properly understand differences in student performance across a diverse population, and hence to design more effective instruction, it is important to do statistical analyses that take multiple variables into account. It also illustrates the importance of having measures that are sensitive to both subject specific and more general preparation. The results suggest that better matching of the course design and teaching to the incoming student preparation will likely be the most effective way to eliminate observed performance gaps across demographic groups while also improving the success of all students.
△ Less
Submitted 1 May, 2019;
originally announced May 2019.
-
Discriminating Original Region from Duplicated One in Copy-Move Forgery
Authors:
Saba Salehi,
Ahmad Mahmoodi-Aznaveh
Abstract:
Since images are used as evidence in many cases, validation of digital images is essential. Copy-move forgery is a special kind of manipulation in which some parts of an image is copied and pasted into another part of the same image. Various methods have been proposed to detect copy-move forgery, which have achieved promising results. In previous methods, a binary mask determining the original and…
▽ More
Since images are used as evidence in many cases, validation of digital images is essential. Copy-move forgery is a special kind of manipulation in which some parts of an image is copied and pasted into another part of the same image. Various methods have been proposed to detect copy-move forgery, which have achieved promising results. In previous methods, a binary mask determining the original and forged region is presented as the final result. However, it is not specified which part of the mask is the forged region. It should be noted that discriminating the original region from the duplicated one is not usually feasible by human visual system(HVS). On the other hand, exact localizing the forged region can be helpful for automatic forgery detection especially in combined forgeries. In real-world forgeries, some manipulations are performed in order to provide a visibly realistic scene. These modifications are usually applied on the boundary of the duplicated snippets. In this research, the texture information of the border regions of both the original and copied patches have been statistically investigated. Based on this analysis, we propose a method to discriminated copied snippets from original ones. In order to validate our method, GRIP dataset is utilized since it contains more realistic forged images which are not easily recognizable by HVS.
△ Less
Submitted 17 March, 2019;
originally announced March 2019.
-
Clockless Spin-based Look-Up Tables with Wide Read Margin
Authors:
Soheil Salehi,
Ramtin Zand,
Ronald F. DeMara
Abstract:
In this paper, we develop a 6-input fracturable non-volatile Clockless LUT (C-LUT) using spin Hall effect (SHE)-based Magnetic Tunnel Junctions (MTJs) and provide a detailed comparison between the SHE-MTJ-based C-LUT and Spin Transfer Torque (STT)-MTJ-based C-LUT. The proposed C-LUT offers an attractive alternative for implementing combinational logic as well as sequential logic versus previous sp…
▽ More
In this paper, we develop a 6-input fracturable non-volatile Clockless LUT (C-LUT) using spin Hall effect (SHE)-based Magnetic Tunnel Junctions (MTJs) and provide a detailed comparison between the SHE-MTJ-based C-LUT and Spin Transfer Torque (STT)-MTJ-based C-LUT. The proposed C-LUT offers an attractive alternative for implementing combinational logic as well as sequential logic versus previous spin-based LUT designs in the literature. Foremost, C-LUT eliminates the sense amplifier typically employed by using a differential polarity dual MTJ design, as opposed to a static reference resistance MTJ. This realizes a much wider read margin and the Monte Carlo simulation of the proposed fracturable C-LUT indicates no read and write errors in the presence of a variety of process variations scenarios involving MOS transistors as well as MTJs. Additionally, simulation results indicate that the proposed C-LUT reduces the standby power dissipation by 5.4-fold compared to the SRAM-based LUT. Furthermore, the proposed SHE-MTJ-based C-LUT reduces the area by 1.3-fold and 2-fold compared to the SRAM-based LUT and the STT-MTJ-based C-LUT, respectively.
△ Less
Submitted 12 March, 2019; v1 submitted 3 March, 2019;
originally announced March 2019.
-
AQuRate: MRAM-based Stochastic Oscillator for Adaptive Quantization Rate Sampling of Sparse Signals
Authors:
Soheil Salehi,
Ramtin Zand,
Alireza Zaeemzadeh,
Nazanin Rahnavard,
Ronald F. DeMara
Abstract:
Recently, the promising aspects of compressive sensing have inspired new circuit-level approaches for their efficient realization within the literature. However, most of these recent advances involving novel sampling techniques have been proposed without considering hardware and signal constraints. Additionally, traditional hardware designs for generating non-uniform sampling clock incur large are…
▽ More
Recently, the promising aspects of compressive sensing have inspired new circuit-level approaches for their efficient realization within the literature. However, most of these recent advances involving novel sampling techniques have been proposed without considering hardware and signal constraints. Additionally, traditional hardware designs for generating non-uniform sampling clock incur large area overhead and power dissipation. Herein, we propose a novel non-uniform clock generator called Adaptive Quantization Rate (AQR) generator using Magnetic Random Access Memory (MRAM)-based stochastic oscillator devices. Our proposed AQR generator provides ~25-fold reduction in area, on average, while offering ~6-fold reduced power dissipation, on average, compared to the state-of-the-art non-uniform clock generators.
△ Less
Submitted 12 March, 2019; v1 submitted 3 March, 2019;
originally announced March 2019.
-
First-Order Continuous Induction, and a Logical Study of Real Closed Fields
Authors:
Saeed Salehi,
Mohammadsaleh Zarza
Abstract:
Over the last century, the principle of "induction on the continuum" has been studied by different authors in different formats. All of these different readings are equivalent to one of the three versions that we isolate in this paper. We also formalize those three forms (of "continuous induction") in first-order logic and prove that two of them are equivalent and sufficiently strong to completely…
▽ More
Over the last century, the principle of "induction on the continuum" has been studied by different authors in different formats. All of these different readings are equivalent to one of the three versions that we isolate in this paper. We also formalize those three forms (of "continuous induction") in first-order logic and prove that two of them are equivalent and sufficiently strong to completely axiomatize the first-order theory of the real closed (ordered) fields. We show that the third weaker form of continuous induction is equivalent with the Archimedean property. We study some equivalent axiomatizations for the theory of real closed fields and propose a first-order scheme of the fundamental theorem of algebra as an alternative axiomatization for this theory (over the theory of ordered fields).
△ Less
Submitted 11 April, 2019; v1 submitted 1 November, 2018;
originally announced November 2018.
-
Traffic Differentiation in Dense WLANs with CSMA/ECA-DR MAC Protocol
Authors:
Seyedmohammad Salehi,
Li Li,
Chien-Chung Shen,
Leonard Cimini,
John Graybeal
Abstract:
In today's WLANs, scheduling of packet transmissions solely relies on the collision and success a station may experience. To better support traffic differentiation in dense WLANs, in this paper, we propose a distributed reservation mechanism for the Carrier Sense Multiple Access Extended Collision Avoidance (CSMA/ECA) MAC protocol, termed CSMA/ECA-DR, based on which stations can collaboratively ac…
▽ More
In today's WLANs, scheduling of packet transmissions solely relies on the collision and success a station may experience. To better support traffic differentiation in dense WLANs, in this paper, we propose a distributed reservation mechanism for the Carrier Sense Multiple Access Extended Collision Avoidance (CSMA/ECA) MAC protocol, termed CSMA/ECA-DR, based on which stations can collaboratively achieve higher network performance. In addition, proper Contention Window (CW) will be chosen based on the instantaneously estimated number of active contenders in the network. Simulation results from dense scenarios with traffic differentiation demonstrate that CSMA/ECA-DR can greatly improve the efficiency of WLANs for traffic differentiation even with large numbers of contenders.
△ Less
Submitted 25 June, 2018;
originally announced June 2018.
-
Optoelectronic properties of defective MoS$_2$ and WS$_2$ monolayers
Authors:
Saboura Salehi,
Alireza Saffarzadeh
Abstract:
We theoretically explore the effect of metal and disulphur vacancies on electronic and optical properties of MoS$_2$ and WS$_2$ monolayers based on a Slater-Koster tight-binding model and including the spin-orbit coupling. We show that the vacancy defects create electronic flat bands by shifting the Fermi level towards the valence band, indicating that both types of vacancies may act as acceptor s…
▽ More
We theoretically explore the effect of metal and disulphur vacancies on electronic and optical properties of MoS$_2$ and WS$_2$ monolayers based on a Slater-Koster tight-binding model and including the spin-orbit coupling. We show that the vacancy defects create electronic flat bands by shifting the Fermi level towards the valence band, indicating that both types of vacancies may act as acceptor sites. The optical spectra of the pristine monolayers show step-like features corresponding to the transition from spin split valence band to the conduction band minimum, whereas the defective monolayers exhibit additional peaks in their spectra arising from induced midgap states in their band structures. We find that Mo and W vacancies contribute mostly in the low-energy optical spectrum, while the S$_2$ vacancies enhance the optical conductivity mainly in the visible range of the spectrum. This suggests that depending on the type of vacancy, the atomic defects in MoS$_2$ and WS$_2$ monolayers may increase the efficiency of solar cells used in photovoltaic systems.
△ Less
Submitted 24 May, 2018;
originally announced May 2018.
-
Asymmetric Loss Functions and Deep Densely Connected Networks for Highly Imbalanced Medical Image Segmentation: Application to Multiple Sclerosis Lesion Detection
Authors:
Seyed Raein Hashemi,
Seyed Sadegh Mohseni Salehi,
Deniz Erdogmus,
Sanjay P. Prabhu,
Simon K. Warfield,
Ali Gholipour
Abstract:
Fully convolutional deep neural networks have been asserted to be fast and precise frameworks with great potential in image segmentation. One of the major challenges in training such networks raises when data is unbalanced, which is common in many medical imaging applications such as lesion segmentation where lesion class voxels are often much lower in numbers than non-lesion voxels. A trained net…
▽ More
Fully convolutional deep neural networks have been asserted to be fast and precise frameworks with great potential in image segmentation. One of the major challenges in training such networks raises when data is unbalanced, which is common in many medical imaging applications such as lesion segmentation where lesion class voxels are often much lower in numbers than non-lesion voxels. A trained network with unbalanced data may make predictions with high precision and low recall, being severely biased towards the non-lesion class which is particularly undesired in most medical applications where FNs are more important than FPs. Various methods have been proposed to address this problem, more recently similarity loss functions and focal loss. In this work we trained fully convolutional deep neural networks using an asymmetric similarity loss function to mitigate the issue of data imbalance and achieve much better tradeoff between precision and recall. To this end, we developed a 3D FC-DenseNet with large overlap** image patches as input and an asymmetric similarity loss layer based on Tversky index (using Fbeta scores). We used large overlap** image patches as inputs for intrinsic and extrinsic data augmentation, a patch selection algorithm, and a patch prediction fusion strategy using B-spline weighted soft voting to account for the uncertainty of prediction in patch borders. We applied this method to MS lesion segmentation based on two different datasets of MSSEG and ISBI longitudinal MS lesion segmentation challenge, where we achieved top performance in both challenges. Our network trained with focal loss ranked first according to the ISBI challenge overall score and resulted in the lowest reported lesion false positive rate among all submitted methods. Our network trained with the asymmetric similarity loss led to the lowest surface distance and the best lesion true positive rate.
△ Less
Submitted 13 December, 2018; v1 submitted 28 March, 2018;
originally announced March 2018.
-
Real-time Deep Pose Estimation with Geodesic Loss for Image-to-Template Rigid Registration
Authors:
Seyed Sadegh Mohseni Salehi,
Shadab Khan,
Deniz Erdogmus,
Ali Gholipour
Abstract:
With an aim to increase the capture range and accelerate the performance of state-of-the-art inter-subject and subject-to-template 3D registration, we propose deep learning-based methods that are trained to find the 3D position of arbitrarily oriented subjects or anatomy based on slices or volumes of medical images. For this, we propose regression CNNs that learn to predict the angle-axis represen…
▽ More
With an aim to increase the capture range and accelerate the performance of state-of-the-art inter-subject and subject-to-template 3D registration, we propose deep learning-based methods that are trained to find the 3D position of arbitrarily oriented subjects or anatomy based on slices or volumes of medical images. For this, we propose regression CNNs that learn to predict the angle-axis representation of 3D rotations and translations using image features. We use and compare mean square error and geodesic loss to train regression CNNs for 3D pose estimation used in two different scenarios: slice-to-volume registration and volume-to-volume registration. Our results show that in such registration applications that are amendable to learning, the proposed deep learning methods with geodesic loss minimization can achieve accurate results with a wide capture range in real-time (<100ms). We also tested the generalization capability of the trained CNNs on an expanded age range and on images of newborn subjects with similar and different MR image contrasts. We trained our models on T2-weighted fetal brain MRI scans and used them to predict the 3D pose of newborn brains based on T1-weighted MRI scans. We showed that the trained models generalized well for the new domain when we performed image contrast transfer through a conditional generative adversarial network. This indicates that the domain of application of the trained deep regression CNNs can be further expanded to image modalities and contrasts other than those used in training. A combination of our proposed methods with accelerated optimization-based registration algorithms can dramatically enhance the performance of automatic imaging devices and image processing methods of the future.
△ Less
Submitted 18 August, 2018; v1 submitted 15 March, 2018;
originally announced March 2018.
-
Real-Time Automatic Fetal Brain Extraction in Fetal MRI by Deep Learning
Authors:
Seyed Sadegh Mohseni Salehi,
Seyed Raein Hashemi,
Clemente Velasco-Annis,
Abdelhakim Ouaalam,
Judy A. Estroff,
Deniz Erdogmus,
Simon K. Warfield,
Ali Gholipour
Abstract:
Brain segmentation is a fundamental first step in neuroimage analysis. In the case of fetal MRI, it is particularly challenging and important due to the arbitrary orientation of the fetus, organs that surround the fetal head, and intermittent fetal motion. Several promising methods have been proposed but are limited in their performance in challenging cases and in real-time segmentation. We aimed…
▽ More
Brain segmentation is a fundamental first step in neuroimage analysis. In the case of fetal MRI, it is particularly challenging and important due to the arbitrary orientation of the fetus, organs that surround the fetal head, and intermittent fetal motion. Several promising methods have been proposed but are limited in their performance in challenging cases and in real-time segmentation. We aimed to develop a fully automatic segmentation method that independently segments sections of the fetal brain in 2D fetal MRI slices in real-time. To this end, we developed and evaluated a deep fully convolutional neural network based on 2D U-net and autocontext, and compared it to two alternative fast methods based on 1) a voxelwise fully convolutional network and 2) a method based on SIFT features, random forest and conditional random field. We trained the networks with manual brain masks on 250 stacks of training images, and tested on 17 stacks of normal fetal brain images as well as 18 stacks of extremely challenging cases based on extreme motion, noise, and severely abnormal brain shape. Experimental results show that our U-net approach outperformed the other methods and achieved average Dice metrics of 96.52% and 78.83% in the normal and challenging test sets, respectively. With an unprecedented performance and a test run time of about 1 second, our network can be used to segment the fetal brain in real-time while fetal MRI slices are being acquired. This can enable real-time motion tracking, motion detection, and 3D reconstruction of fetal brain MRI.
△ Less
Submitted 25 October, 2017;
originally announced October 2017.
-
On Decidability of the Ordered Structures of Numbers
Authors:
Ziba Assadi,
Saeed Salehi
Abstract:
The ordered structures of natural, integer, rational and real numbers are studied here. It is known that the theories of these numbers in the language of order are decidable and finitely axiomatizable. Also, their theories in the language of order and addition are decidable and infinitely axiomatizable. For the language of order and multiplication, it is known that the theories of $\mathbb{N}$ and…
▽ More
The ordered structures of natural, integer, rational and real numbers are studied here. It is known that the theories of these numbers in the language of order are decidable and finitely axiomatizable. Also, their theories in the language of order and addition are decidable and infinitely axiomatizable. For the language of order and multiplication, it is known that the theories of $\mathbb{N}$ and $\mathbb{Z}$ are not decidable (and so not axiomatizable by any computably enumerable set of sentences). By Tarski's theorem, the multiplicative ordered structure of $\mathbb{R}$ is decidable also; here we prove this result directly and present an axiomatization. The structure of $\mathbb{Q}$ in the language of order and multiplication seems to be missing in the literature; here we show the decidability of its theory by the technique of quantifier elimination and after presenting an infinite axiomatization for this structure we prove that it is not finitely axiomatizable.
△ Less
Submitted 14 February, 2018; v1 submitted 15 September, 2017;
originally announced September 2017.
-
On Axiomatizability of the Multiplicative Theory of Numbers
Authors:
Saeed Salehi
Abstract:
The multiplicative theory of a set of numbers (which could be natural, integer, rational, real or complex numbers) is the first-order theory of the structure of that set with (solely) the multiplication operation (that set is taken to be multiplicative, i.e., closed under multiplication). In this paper we study the multiplicative theories of the complex, real and (positive) rational numbers. These…
▽ More
The multiplicative theory of a set of numbers (which could be natural, integer, rational, real or complex numbers) is the first-order theory of the structure of that set with (solely) the multiplication operation (that set is taken to be multiplicative, i.e., closed under multiplication). In this paper we study the multiplicative theories of the complex, real and (positive) rational numbers. These theories (and also the multiplicative theories of natural and integer numbers) are known to be decidable (i.e., there exists an algorithm that decides whether a given sentence is derivable form the theory); here we present explicit axiomatizations for them and show that they are not finitely axiomatizable. For each of these sets (of complex, real and [positive] rational numbers) a language, including the multiplication operation, is introduced in a way that it allows quantifier elimination (for the theory of that set).
△ Less
Submitted 14 February, 2018; v1 submitted 15 July, 2017;
originally announced July 2017.
-
Tversky loss function for image segmentation using 3D fully convolutional deep networks
Authors:
Seyed Sadegh Mohseni Salehi,
Deniz Erdogmus,
Ali Gholipour
Abstract:
Fully convolutional deep neural networks carry out excellent potential for fast and accurate image segmentation. One of the main challenges in training these networks is data imbalance, which is particularly problematic in medical imaging applications such as lesion segmentation where the number of lesion voxels is often much lower than the number of non-lesion voxels. Training with unbalanced dat…
▽ More
Fully convolutional deep neural networks carry out excellent potential for fast and accurate image segmentation. One of the main challenges in training these networks is data imbalance, which is particularly problematic in medical imaging applications such as lesion segmentation where the number of lesion voxels is often much lower than the number of non-lesion voxels. Training with unbalanced data can lead to predictions that are severely biased towards high precision but low recall (sensitivity), which is undesired especially in medical applications where false negatives are much less tolerable than false positives. Several methods have been proposed to deal with this problem including balanced sampling, two step training, sample re-weighting, and similarity loss functions. In this paper, we propose a generalized loss function based on the Tversky index to address the issue of data imbalance and achieve much better trade-off between precision and recall in training 3D fully convolutional deep neural networks. Experimental results in multiple sclerosis lesion segmentation on magnetic resonance images show improved F2 score, Dice coefficient, and the area under the precision-recall curve in test data. Based on these results we suggest Tversky loss function as a generalized framework to effectively train deep neural networks.
△ Less
Submitted 18 June, 2017;
originally announced June 2017.
-
Context-Aware Recursive Bayesian Graph Traversal in BCIs
Authors:
Seyed Sadegh Mohseni Salehi,
Mohammad Moghadamfalahi,
Hooman Nezamfar,
Marzieh Haghighi,
Deniz Erdogmus
Abstract:
Noninvasive brain computer interfaces (BCI), and more specifically Electroencephalography (EEG) based systems for intent detection need to compensate for the low signal to noise ratio of EEG signals. In many applications, the temporal dependency information from consecutive decisions and contextual data can be used to provide a prior probability for the upcoming decision. In this study we proposed…
▽ More
Noninvasive brain computer interfaces (BCI), and more specifically Electroencephalography (EEG) based systems for intent detection need to compensate for the low signal to noise ratio of EEG signals. In many applications, the temporal dependency information from consecutive decisions and contextual data can be used to provide a prior probability for the upcoming decision. In this study we proposed two probabilistic graphical models (PGMs), using context information and previously observed EEG evidences to estimate a probability distribution over the decision space in graph based decision-making mechanism. In this approach, user moves a pointer to the desired vertex in the graph in which each vertex represents an action. To select a vertex, a Select command, or a proposed probabilistic Selection criterion (PSC) can be used to automatically detect the user intended vertex. Performance of different PGMs and Selection criteria combinations are compared over a keyboard based on a graph layout. Based on the simulation results, probabilistic Selection criterion along with the probabilistic graphical model provides the highest performance boost for individuals with pour calibration performance and achieving the same performance for individuals with high calibration performance.
△ Less
Submitted 8 March, 2017;
originally announced March 2017.
-
Decoding Complex Imagery Hand Gestures
Authors:
Seyed Sadegh Mohseni Salehi,
Mohammad Moghadamfalahi,
Fernando Quivira,
Alexander Piers,
Hooman Nezamfar,
Deniz Erdogmus
Abstract:
Brain computer interfaces (BCIs) offer individuals suffering from major disabilities an alternative method to interact with their environment. Sensorimotor rhythm (SMRs) based BCIs can successfully perform control tasks; however, the traditional SMR paradigms intuitively disconnect the control and real task, making them non-ideal for complex control scenarios. In this study, we design a new, intui…
▽ More
Brain computer interfaces (BCIs) offer individuals suffering from major disabilities an alternative method to interact with their environment. Sensorimotor rhythm (SMRs) based BCIs can successfully perform control tasks; however, the traditional SMR paradigms intuitively disconnect the control and real task, making them non-ideal for complex control scenarios. In this study, we design a new, intuitively connected motor imagery (MI) paradigm using hierarchical common spatial patterns (HCSP) and context information to effectively predict intended hand grasps from electroencephalogram (EEG) data. Experiments with 5 participants yielded an aggregate classification accuracy--intended grasp prediction probability--of 64.5\% for 8 different hand gestures, more than 5 times the chance level.
△ Less
Submitted 8 March, 2017;
originally announced March 2017.
-
Auto-context Convolutional Neural Network (Auto-Net) for Brain Extraction in Magnetic Resonance Imaging
Authors:
Seyed Sadegh Mohseni Salehi,
Deniz Erdogmus,
Ali Gholipour
Abstract:
Brain extraction or whole brain segmentation is an important first step in many of the neuroimage analysis pipelines. The accuracy and robustness of brain extraction, therefore, is crucial for the accuracy of the entire brain analysis process. With the aim of designing a learning-based, geometry-independent and registration-free brain extraction tool in this study, we present a technique based on…
▽ More
Brain extraction or whole brain segmentation is an important first step in many of the neuroimage analysis pipelines. The accuracy and robustness of brain extraction, therefore, is crucial for the accuracy of the entire brain analysis process. With the aim of designing a learning-based, geometry-independent and registration-free brain extraction tool in this study, we present a technique based on an auto-context convolutional neural network (CNN), in which intrinsic local and global image features are learned through 2D patches of different window sizes. In this architecture three parallel 2D convolutional pathways for three different directions (axial, coronal, and sagittal) implicitly learn 3D image information without the need for computationally expensive 3D convolutions. Posterior probability maps generated by the network are used iteratively as context information along with the original image patches to learn the local shape and connectedness of the brain, to extract it from non-brain tissue.
The brain extraction results we have obtained from our algorithm are superior to the recently reported results in the literature on two publicly available benchmark datasets, namely LPBA40 and OASIS, in which we obtained Dice overlap coefficients of 97.42% and 95.40%, respectively. Furthermore, we evaluated the performance of our algorithm in the challenging problem of extracting arbitrarily-oriented fetal brains in reconstructed fetal brain magnetic resonance imaging (MRI) datasets. In this application our algorithm performed much better than the other methods (Dice coefficient: 95.98%), where the other methods performed poorly due to the non-standard orientation and geometry of the fetal brain in MRI. Our CNN-based method can provide accurate, geometry-independent brain extraction in challenging applications.
△ Less
Submitted 19 June, 2017; v1 submitted 6 March, 2017;
originally announced March 2017.
-
Computation in Logic and Logic in Computation
Authors:
Saeed Salehi
Abstract:
The theory of addition in the domains of natural (N), integer (Z), rational (Q), real (R) and complex (C) numbers is decidable, so is the theory of multiplication in all those domains. By Godel's Incompleteness Theorem the theory of addition and multiplication is undecidable in the domains of N, Z and Q, though Tarski proved that this theory is decidable in the domains of R and C. The theory of mu…
▽ More
The theory of addition in the domains of natural (N), integer (Z), rational (Q), real (R) and complex (C) numbers is decidable, so is the theory of multiplication in all those domains. By Godel's Incompleteness Theorem the theory of addition and multiplication is undecidable in the domains of N, Z and Q, though Tarski proved that this theory is decidable in the domains of R and C. The theory of multiplication and order (x,<) behaves differently in the above mentioned domains of numbers. By a theorem of Robinson, addition is definable by multiplication and order in the domain of natural numbers, thus the theory (N;x,<) is undecidable. By a classical theorem in mathematical logic, addition is not definable in terms of multiplication and order in R. In this paper, we extend Robinson's theorem to the domain of integers (Z) by showing the definability of addition in (Z;x,<), this implies that (Z;x,<) is undecidable. We also show the decidability of (Q;x,<) by the method of quantifier elimination. Whence, addition is not definable in (Q;x,<).
△ Less
Submitted 20 December, 2016;
originally announced December 2016.
-
Axiomatizing Mathematical Theories: Multiplication
Authors:
Saeed Salehi
Abstract:
Axiomatizing mathematical structures is a goal of Mathematical Logic. Axiomatizability of the theories of some structures have turned out to be quite difficult and challenging, and some remain open. However axiomatization of some mathematical structures are now classical theorems in Logic, Algebra and Geometry. In this paper we will study the axiomatizability of the theories of multiplication in t…
▽ More
Axiomatizing mathematical structures is a goal of Mathematical Logic. Axiomatizability of the theories of some structures have turned out to be quite difficult and challenging, and some remain open. However axiomatization of some mathematical structures are now classical theorems in Logic, Algebra and Geometry. In this paper we will study the axiomatizability of the theories of multiplication in the domains of natural, integer, rational, real, and complex numbers. We will review some classical theorems, and will give some new proofs for old results. We will see that some structures are missing in the literature, thus leaving it open whether the theories of that structures are axiomatizable (decidable) or not. We will answer one of those open questions in this paper.
△ Less
Submitted 20 December, 2016;
originally announced December 2016.
-
On Constructivity and the Rosser Property: a closer look at some Gödelean proofs
Authors:
Saeed Salehi,
Payam Seraji
Abstract:
The proofs of Kleene, Chaitin and Boolos for Gödel's First Incompleteness Theorem are studied from the perspectives of constructivity and the Rosser property. A proof of the incompleteness theorem has the Rosser property when the independence of the true but unprovable sentence can be shown by assuming only the (simple) consistency of the theory. It is known that Gödel's own proof for his incomple…
▽ More
The proofs of Kleene, Chaitin and Boolos for Gödel's First Incompleteness Theorem are studied from the perspectives of constructivity and the Rosser property. A proof of the incompleteness theorem has the Rosser property when the independence of the true but unprovable sentence can be shown by assuming only the (simple) consistency of the theory. It is known that Gödel's own proof for his incompleteness theorem does not have the Rosser property, and we show that neither do Kleene's or Boolos' proofs. However, we show that a variant of Chaitin's proof can have the Rosser property. The proofs of Gödel, Rosser and Kleene are constructive in the sense that they explicitly construct, by algorithmic ways, the independent sentence(s) from the theory. We show that the proofs of Chaitin and Boolos are not constructive, and they prove only the mere existence of the independent sentences.
△ Less
Submitted 14 February, 2018; v1 submitted 8 December, 2016;
originally announced December 2016.
-
Kripke Semantics for Fuzzy Logics
Authors:
Parvin Safari,
Saeed Salehi
Abstract:
Kripke frames (and models) provide a suitable semantics for sub-classical logics, for example Intuitionistic Logic (of Brouwer and Heyting) axiomatizes the reflexive and transitive Kripke frames (with persistent satisfaction relations), and the Basic Logic (of Visser) axiomatizes transitive Kripke frames (with persistent satisfaction relations). Here, we investigate whether Kripke frames/models co…
▽ More
Kripke frames (and models) provide a suitable semantics for sub-classical logics, for example Intuitionistic Logic (of Brouwer and Heyting) axiomatizes the reflexive and transitive Kripke frames (with persistent satisfaction relations), and the Basic Logic (of Visser) axiomatizes transitive Kripke frames (with persistent satisfaction relations). Here, we investigate whether Kripke frames/models could provide a semantics for fuzzy logics. For each axiom of the Basic Fuzzy Logic, necessary and sufficient conditions are sought for Kripke frames/models which satisfy them. It turns out that the only fuzzy logics (logics containing the Basic Fuzzy Logic) which are sound and complete with respect to a class of Kripke frames/models are the extensions of the Gödel Logic (or the super-intuitionistic logic of Dummett), indeed this logic is sound and strongly complete with respect to reflexive, transitive and connected (linear) Kripke frames (with persistent satisfaction relations). This provides a semantic characterization for the Gödel Logic among (propositional) fuzzy logics.
△ Less
Submitted 10 December, 2016; v1 submitted 14 July, 2016;
originally announced July 2016.
-
On Arithmetical Truth of the Self-Referential Sentences
Authors:
Kaave Lajevardi,
Saeed Salehi
Abstract:
We take an argument of Gödel's from his ground-breaking 1931 paper, generalize it, and examine its validity. The argument in question is this: the sentence $G$ says about itself that it is not provable, and $G$ is indeed not provable; therefore, $G$ is true.
We take an argument of Gödel's from his ground-breaking 1931 paper, generalize it, and examine its validity. The argument in question is this: the sentence $G$ says about itself that it is not provable, and $G$ is indeed not provable; therefore, $G$ is true.
△ Less
Submitted 14 February, 2018; v1 submitted 14 July, 2016;
originally announced July 2016.
-
Atomic defect states in monolayers of MoS$_2$ and WS$_2$
Authors:
Saboura Salehi,
Alireza Saffarzadeh
Abstract:
The influence of atomic vacancy defects at different concentrations on electronic properties of MoS$_2$ and WS$_2$ monolayers is studied by means of Slater-Koster tight-binding model with non-orthogonal $sp^3d^5$ orbitals and including the spin-orbit coupling. The presence of vacancy defects induces localized states in the bandgap of pristine MoS$_2$ and WS$_2$, which have potential to modify the…
▽ More
The influence of atomic vacancy defects at different concentrations on electronic properties of MoS$_2$ and WS$_2$ monolayers is studied by means of Slater-Koster tight-binding model with non-orthogonal $sp^3d^5$ orbitals and including the spin-orbit coupling. The presence of vacancy defects induces localized states in the bandgap of pristine MoS$_2$ and WS$_2$, which have potential to modify the electronic structure of the systems, depending on the type and concentration of the defects. It is shown that although the contribution of metal (Mo or W) $d$ orbitals is dominant in the formation of midgap states, the sulphur $p$ and $d$ orbitals have also considerable contribution in the localized states, when metal defects are introduced. Our results suggest that Mo and W defects can turn the monolayers into p-type semiconductors, while the sulphur defects make the system a n-type semiconductor, in agreement with ab initio results and experimental observations.
△ Less
Submitted 27 May, 2016;
originally announced May 2016.
-
Theorems of Tarski's Undefinability and Godel's Second Incompleteness-Computationally
Authors:
Saeed Salehi
Abstract:
We present a version of Gödel's Second Incompleteness Theorem for recursively enumerable consistent extensions of a fixed axiomatizable theory, by incorporating some bi-theoretic version of the derivability conditions. We also argue that Tarski's theorem on the Undefinability of Truth is Gödel's First Incompleteness Theorem relativized to definable oracles; a unification of these two theorems is g…
▽ More
We present a version of Gödel's Second Incompleteness Theorem for recursively enumerable consistent extensions of a fixed axiomatizable theory, by incorporating some bi-theoretic version of the derivability conditions. We also argue that Tarski's theorem on the Undefinability of Truth is Gödel's First Incompleteness Theorem relativized to definable oracles; a unification of these two theorems is given.
△ Less
Submitted 10 November, 2019; v1 submitted 1 September, 2015;
originally announced September 2015.
-
Godel-Rosser's Incompleteness Theorems for Non-Recursively Enumerable Theories
Authors:
Saeed Salehi,
Payam Seraji
Abstract:
Godel's First Incompleteness Theorem is generalized to definable theories, which are not necessarily recursively enumerable, by using a couple of syntactic-semantic notions, one is the consistency of a theory with the set of all true $Π_n$-sentences or equivalently the $Σ_n$-soundness of the theory, and the other is $n$-consistency the restriction of $ω$-consistency to the $Σ_n$-formulas. It is al…
▽ More
Godel's First Incompleteness Theorem is generalized to definable theories, which are not necessarily recursively enumerable, by using a couple of syntactic-semantic notions, one is the consistency of a theory with the set of all true $Π_n$-sentences or equivalently the $Σ_n$-soundness of the theory, and the other is $n$-consistency the restriction of $ω$-consistency to the $Σ_n$-formulas. It is also shown that Rosser's Incompleteness Theorem does not generally hold for definable non-recursively enumerable theories, whence Godel-Rosser's Incompleteness Theorem is optimal in a sense. Though the proof of the incompleteness theorem using the $Σ_n$-soundness assumption is constructive, it is shown that there is no constructive proof for the incompleteness theorem using the $n$-consistency assumption, for $n\!>\!2$.
△ Less
Submitted 10 December, 2016; v1 submitted 9 June, 2015;
originally announced June 2015.
-
Position probability density function for a system of mutually exclusive particles in one dimension
Authors:
Rasool Kheiry,
Shahram Salehi
Abstract:
Position probability distribution of a set of massive mutually exclusive particles in one dimension has been defined. Examples with a given two mutually exclusive particles system are considered. It is emphasized that quantum particles at finite potentials can not be regarded as a mutually exclusive system or they are indistinguishable. Afterward, it is attempted to ascribe a mutually exclusive sy…
▽ More
Position probability distribution of a set of massive mutually exclusive particles in one dimension has been defined. Examples with a given two mutually exclusive particles system are considered. It is emphasized that quantum particles at finite potentials can not be regarded as a mutually exclusive system or they are indistinguishable. Afterward, it is attempted to ascribe a mutually exclusive system to continuous mass densities of a rigid body to calculate average values. We do this by applying correspondence principle with regard to probability densities.
△ Less
Submitted 26 October, 2016; v1 submitted 24 October, 2014;
originally announced October 2014.
-
Theoremizing Yablo's Paradox
Authors:
Ahmad Karimi,
Saeed Salehi
Abstract:
To counter a general belief that all the paradoxes stem from a kind of circularity (or involve some self--reference, or use a diagonal argument) Stephen Yablo designed a paradox in 1993 that seemingly avoided self--reference. We turn Yablo's paradox, the most challenging paradox in the recent years, into a genuine mathematical theorem in Linear Temporal Logic (LTL). Indeed, Yablo's paradox comes i…
▽ More
To counter a general belief that all the paradoxes stem from a kind of circularity (or involve some self--reference, or use a diagonal argument) Stephen Yablo designed a paradox in 1993 that seemingly avoided self--reference. We turn Yablo's paradox, the most challenging paradox in the recent years, into a genuine mathematical theorem in Linear Temporal Logic (LTL). Indeed, Yablo's paradox comes in several varieties; and he showed in 2004 that there are other versions that are equally paradoxical. Formalizing these versions of Yablo's paradox, we prove some theorems in LTL. This is the first time that Yablo's paradox(es) become new(ly discovered) theorems in mathematics and logic.
△ Less
Submitted 1 June, 2014;
originally announced June 2014.
-
Diagonalizing by Fixed-Points
Authors:
Ahmad Karimi,
Saeed Salehi
Abstract:
A universal schema for diagonalization was popularized by N. S. Yanofsky (2003) in which the existence of a (diagonolized-out and contradictory) object implies the existence of a fixed-point for a certain function. It was shown that many self-referential paradoxes and diagonally proved theorems can fit in that schema. Here, we fit more theorems in the universal schema of diagonalization, such as E…
▽ More
A universal schema for diagonalization was popularized by N. S. Yanofsky (2003) in which the existence of a (diagonolized-out and contradictory) object implies the existence of a fixed-point for a certain function. It was shown that many self-referential paradoxes and diagonally proved theorems can fit in that schema. Here, we fit more theorems in the universal schema of diagonalization, such as Euclid's theorem on the infinitude of the primes and new proofs of Boolos (1997) for Cantor's theorem on the non-equinumerosity of a set with its powerset. Then, in Linear Temporal Logic, we show the non-existence of a fixed-point in this logic whose proof resembles the argument of Yablo's paradox. Thus, Yablo's paradox turns for the first time into a genuine mathematico-logical theorem in the framework of Linear Temporal Logic. Again the diagonal schema of the paper is used in this proof, and also it is shown that G. Priest's inclosure schema (1997) can fit in our universal diagonal/fixed-point schema. We also show the existence of dominating (Ackermann-like) functions (which dominate a given countable set of functions---like primitive recursives) using the schema.
△ Less
Submitted 10 December, 2016; v1 submitted 4 March, 2013;
originally announced March 2013.
-
Godel's Incompleteness Phenomenon - Computationally
Authors:
Saeed Salehi
Abstract:
We argue that Godel's completeness theorem is equivalent to completability of consistent theories, and Godel's incompleteness theorem is equivalent to the fact that this completion is not constructive, in the sense that there are some consistent and recursively enumerable theories which cannot be extended to any complete and consistent and recursively enumerable theory. Though any consistent and d…
▽ More
We argue that Godel's completeness theorem is equivalent to completability of consistent theories, and Godel's incompleteness theorem is equivalent to the fact that this completion is not constructive, in the sense that there are some consistent and recursively enumerable theories which cannot be extended to any complete and consistent and recursively enumerable theory. Though any consistent and decidable theory can be extended to a complete and consistent and decidable theory. Thus deduction and consistency are not decidable in logic, and an analogue of Rice's Theorem holds for recursively enumerable theories: all the non-trivial properties of such theories are undecidable.
△ Less
Submitted 10 December, 2016; v1 submitted 30 November, 2012;
originally announced November 2012.
-
Herbrand Consistency of Some Finite Fragments of Bounded Arithmetical Theories
Authors:
Saeed Salehi
Abstract:
We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of ${\rm IΔ_0}$ whose Herbrand Consistency is not provable in the thoery ${\rm IΔ_0}$. We also show the existence of an ${\rm IΔ_0}-$derivable $Π_1-$sentence such that ${\rm IΔ_0}$ cannot prove its Herbrand Consistency.
We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of ${\rm IΔ_0}$ whose Herbrand Consistency is not provable in the thoery ${\rm IΔ_0}$. We also show the existence of an ${\rm IΔ_0}-$derivable $Π_1-$sentence such that ${\rm IΔ_0}$ cannot prove its Herbrand Consistency.
△ Less
Submitted 10 December, 2016; v1 submitted 9 October, 2011;
originally announced October 2011.
-
Artificial Skin Ridges Enhance Local Tactile Shape Discrimination
Authors:
Saba Salehi,
John-John Cabibihan,
Shuzhi Sam Ge
Abstract:
One of the fundamental requirements for an artificial hand to successfully grasp and manipulate an object is to be able to distinguish different objects' shapes and, more specifically, the objects' surface curvatures. In this study, we investigate the possibility of enhancing the curvature detection of embedded tactile sensors by proposing a ridged fingertip structure, simulating human fingerprint…
▽ More
One of the fundamental requirements for an artificial hand to successfully grasp and manipulate an object is to be able to distinguish different objects' shapes and, more specifically, the objects' surface curvatures. In this study, we investigate the possibility of enhancing the curvature detection of embedded tactile sensors by proposing a ridged fingertip structure, simulating human fingerprints. In addition, a curvature detection approach based on machine learning methods is proposed to provide the embedded sensors with the ability to discriminate the surface curvature of different objects. For this purpose, a set of experiments were carried out to collect tactile signals from a 2 \times 2 tactile sensor array, then the signals were processed and used for learning algorithms. To achieve the best possible performance for our machine learning approach, three different learning algorithms of Naïve Bayes (NB), Artificial Neural Networks (ANN), and Support Vector Machines (SVM) were implemented and compared for various parameters. Finally, the most accurate method was selected to evaluate the proposed skin structure in recognition of three different curvatures. The results showed an accuracy rate of 97.5% in surface curvature discrimination.
△ Less
Submitted 16 September, 2011;
originally announced September 2011.
-
Separating Bounded Arithmetics by Herbrand Consistency
Authors:
Saeed Salehi
Abstract:
The problem of $Π_1-$separating the hierarchy of bounded arithmetic has been studied in the paper. It is shown that the notion of Herbrand Consistency, in its full generality, cannot $Π_1-$separate the theory ${\rm IΔ_0+\bigwedge_jΩ_j}$ from ${\rm IΔ_0}$; though it can $Π_1-$separate ${\rm IΔ_0+Exp}$ from ${\rm IΔ_0}$. This extends a result of L. A. Kołodziejczyk (2006), by showing the unprovabili…
▽ More
The problem of $Π_1-$separating the hierarchy of bounded arithmetic has been studied in the paper. It is shown that the notion of Herbrand Consistency, in its full generality, cannot $Π_1-$separate the theory ${\rm IΔ_0+\bigwedge_jΩ_j}$ from ${\rm IΔ_0}$; though it can $Π_1-$separate ${\rm IΔ_0+Exp}$ from ${\rm IΔ_0}$. This extends a result of L. A. Kołodziejczyk (2006), by showing the unprovability of the Herbrand Consistency of ${\rm IΔ_0}$ in the theory ${\rm IΔ_0+\bigwedge_jΩ_j}$.
△ Less
Submitted 10 December, 2016; v1 submitted 2 August, 2010;
originally announced August 2010.
-
Herbrand Consistency of Some Arithmetical Theories
Authors:
Saeed Salehi
Abstract:
Gödel's second incompleteness theorem is proved for Herbrand consistency of some arithmetical theories with bounded induction, by using a technique of logarithmic shrinking the witnesses of bounded formulas, due to Z. Adamowicz [Herbrand consistency and bounded arithmetic, \textit{Fundamenta Mathematicae} 171 (2002) 279--292]. In that paper, it was shown that one cannot always shrink the witness o…
▽ More
Gödel's second incompleteness theorem is proved for Herbrand consistency of some arithmetical theories with bounded induction, by using a technique of logarithmic shrinking the witnesses of bounded formulas, due to Z. Adamowicz [Herbrand consistency and bounded arithmetic, \textit{Fundamenta Mathematicae} 171 (2002) 279--292]. In that paper, it was shown that one cannot always shrink the witness of a bounded formula logarithmically, but in the presence of Herbrand consistency, for theories ${\rm IΔ_0+Ω_m}$ with $m\geqslant 2$, any witness for any bounded formula can be shortened logarithmically. This immediately implies the unprovability of Herbrand consistency of a theory $T\supseteq {\rm IΔ_0+Ω_2}$ in $T$ itself.
In this paper, the above results are generalized for ${\rm IΔ_0+Ω_1}$. Also after tailoring the definition of Herbrand consistency for ${\rm IΔ_0}$ we prove the corresponding theorems for ${\rm IΔ_0}$. Thus the Herbrand version of Gödel's second incompleteness theorem follows for the theories ${\rm IΔ_0+Ω_1}$ and ${\rm IΔ_0}$.
△ Less
Submitted 10 December, 2016; v1 submitted 15 May, 2010;
originally announced May 2010.
